Theorem 19.21aiv 1328

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 1012	. 2 |- (ph -> A.xph)
2		19.21aiv.1	. 2 |- (ph -> ps)
3	1, 2	19.21ai 1039	1 |- (ph -> A.xps)

Syntax hints:   -> wi 3  A.wal 995

This theorem is referenced by:  19.21aivv 1329  ax11eq 1405  ax11el 1406  axext4 1507  eqrdv 1520  abbi2dv 1625  abbi1dv 1626  hbeqd 1960  hbeld 1961  moeq3 1968  sbcthdv 1994  sbc2or 2008  sbciegf 2010  hbsbc1gd 2033  hbsbcgd 2034  sbc19.20dv 2035  sbcel12g 2062  sbceqdig 2063  csbnestglem 2086  csbnestg 2087  csbnest1g 2088  ssrdv 2121  abssdv 2172  uniiunlem 2183  disjsn 2493  hbopd 2551  uniss 2575  intss 2608  intab 2614  iunss1 2628  ssiun 2646  hbbrd 2714  axsep 2757  ssopab2 2878  onminex 3077  limom 3203  hbimad 3469  cotr 3493  funco 3607  funun 3611  fununi 3620  funcnvuni 3621  hbfvd 3787  fopab2 3880  iunon 3967  iinon 3968  hboprd 4040  funoprabg 4068  2ndconst 4155  erdisj 4344  mapss 4407  pw2en 4509  unifi 4618  fiint 4620  sucprcreg 4660  aceq3 4795  aceq5 4802  aceq6b 4804  kmlem1 4827  kmlem6 4832  kmlem13 4839  brdom6disj 4867  cfub 4973  cflim 4974  cflecard 4977  1pr 5182  reclem2pr 5222  supexpr 5228  hbnegdi 5428  dfuzi 6287  tgcl 7713  subtop 7733  indistop 7735  neissex 7823  lpval 7828  opntop 7955  ref3w 10566  inposet 10578  cdrci 10588  homeofval 10610  homcard 10633  qusp 10649  fipfil2 10658  cnfilca 10670  ismonc 10824  isepic 10834

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016

Copyright terms: Public domain