Theorem 19.21aiv 1281

Description: Inference from Theorem 19.21 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.21aiv.1	|- (ph -> ps)

Assertion

Ref	Expression
19.21aiv	|- (ph -> A.xps)

Distinct variable group:   ph,x

Proof of Theorem 19.21aiv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		19.21aiv.1	. 2 |- (ph -> ps)
3	1, 2	19.21ai 995	1 |- (ph -> A.xps)

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  19.21aivv 1282  ax11eq 1356  ax11el 1357  eqrdv 1466  abbi2dv 1570  abbi1dv 1571  hbeqd 1904  hbeld 1905  moeq3 1912  sbcthdv 1937  sbc2or 1948  sbciegf 1950  hbsbc1gd 1973  hbsbcgd 1974  sbc19.20dv 1975  sbcel12g 2001  sbceqdig 2002  csbnestglem 2025  csbnestg 2026  csbnest1g 2027  ssrdv 2060  abssdv 2111  uniiunlem 2122  disjsn 2431  hbopd 2488  uniss 2511  intss 2544  intab 2550  iunss1 2564  ssiun 2582  hbbrd 2649  axsep 2692  ssopab2 2811  onminex 3010  limom 3136  hbimad 3396  cotr 3420  funco 3536  funun 3540  fununi 3549  funcnvuni 3550  hbfvd 3715  fopab2 3808  iunon 3894  iinon 3895  hboprd 3967  funoprabg 3995  2ndconst 4081  erdisj 4270  mapss 4330  pw2en 4426  unifi 4532  fiint 4534  sucprcreg 4572  aceq3 4705  aceq5 4712  aceq6b 4714  kmlem1 4737  kmlem6 4742  kmlem13 4749  brdom6disj 4777  cfub 4880  cflim 4881  cflecard 4884  1pr 5089  reclem2pr 5129  supexpr 5135  hbnegd 5335  dfuz 6150  tgclt 7566  subtop 7588  indistop 7590  neissex 7679  lpval 7684  opntop 7810  cdrci 10381  homeofval 10403  homcard 10426  qusp 10430  fipfil2 10439  cnfilca 10451  ismonc 10584

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

Copyright terms: Public domain