Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem 19.23adv 1209

Description: Deduction from Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23adv.1

Assertion

Ref	Expression
19.23adv

Distinct variable groups:   ,   ,

---

Proof of Theorem 19.23adv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2
2		ax-17 968	. 2
3		19.23adv.1	. 2
4	1, 2, 3	19.23ad 1062	1

Colors of variables: wff set class

Syntax hints:   wi 3  wex 977

This theorem is referenced by:  ax11v2 1210  19.23advv 1292  ax11eq 1356  ax11el 1357  ax11inda 1364  sssn 2464  iununi 2606  wefrc 2933  onfr 2976  funfvop 3788  dff2 3802  elunirnALT 3854  isomin 3884  isofrlem 3886  f1oweALT 3891  undom 4418  fodomr 4463  mapen 4471  mapdom2 4474  phplem4 4491  php3 4495  pssnn 4513  ssfi 4515  domfi 4516  isfinite2 4523  fiint 4534  fodomfi 4540  fodomfib 4541  pm54.43 4546  inf3lem2 4586  zfregs 4619  r1pwcl 4659  cplem1 4692  aceq6b 4714  kmlem13 4749  zorn2lem7 4766  fodom 4770  fodomb 4772  unidom 4780  ltexpq 5052  ltbtwnpq 5056  genpnmax 5082  distrlem1pr 5099  1idpr 5105  psslinpr 5107  prlem934 5111  ltaddpr 5112  ltexprlem2 5115  ltexprlem6 5119  ltexprlem7 5120  prlem936 5127  reclem2pr 5129  reclem4pr 5131  suplem1pr 5133  recexsrlem 5184  recexsr 5188  suppsrlem 5193  suppsr2 5195  supsr 5203  suprelem 5231  axrnegex 5255  axrrecex 5256  sup2 5998  infmrcl 6016  fznt 6425  iserzext 7071  isumclim2tf 7133  isumreclt 7145  isummulc1ALT 7148  efseq0ex 7253  acdc2 7432  acdc 7437  infxpidmlem12 7506  tgval3t 7567  tgtopt 7570  basgen2t 7581  subbas2 7587  subtop 7588  metelcls 7900  iscms2lem5 7927  cmsss 7931  bcthlem31 7963  spansncv 9514  hmphsyma 10415  hmphtr 10418

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain