Theorem 19.21aiv 1324

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

Syntax hints:   -> wi 3  A.wal 990

This theorem is referenced by:  19.21aivv 1325  ax11eq 1402  ax11el 1403  axext4 1503  eqrdv 1516  abbi2dv 1621  abbi1dv 1622  hbeqd 1959  hbeld 1960  moeq3 1967  sbcthdv 1992  sbc2or 2006  sbciegf 2008  hbsbc1gd 2031  hbsbcgd 2032  sbc19.20dv 2033  sbcel12g 2062  sbceqdig 2063  csbnestglem 2087  csbnestg 2088  csbnest1g 2089  ssrdv 2122  abssdv 2173  uniiunlem 2184  disjsn 2502  hbopd 2562  uniss 2588  intss 2621  intab 2627  iunss1 2642  ssiun 2660  hbbrd 2732  axsep 2776  ssopab2 2900  onminex 3164  limom 3233  ssrelrel 3340  hbimad 3504  cotr 3528  funco 3655  funun 3659  fununi 3668  funcnvuni 3669  hbfvd 3841  fopab2 3937  hboprd 4040  funoprabg 4070  1stconst 4190  2ndconst 4191  iunon 4207  iinon 4208  erdisj 4426  mapss 4487  pw2en 4587  ac6sfi 4591  unifi 4701  fiint 4703  sucprcreg 4743  aceq3 4879  aceq5 4886  aceq6b 4888  kmlem1 4911  kmlem6 4916  kmlem13 4923  brdom6disj 4951  cfub 5058  cflim 5059  cflecard 5062  1pr 5271  reclem2pr 5311  supexpr 5317  hbnegd 5517  dfuzi 6373  tgcl 7836  subtop 7858  indistop 7860  neissex 7948  lpval 7953  opntop 8080  ref3w 10772  inposet 10868  lteqtpos 10880  homeofval 11022  homcard 11045  qusp 11068  fipfil2 11077  cnfilca 11088  ismonc 11269  isepic 11279  dfiin2g 11400  trer 11409  finminlem 11418  fiss 11419  opncldf1 11454  hscptsscld 11491  alexsublem2 11497  neibastop2lem3 11582  neibastop3 11585  topmtcl 11586  fnemeet2 11590  fnejoin2 11592  filssufillem 11655  filufint 11659  ufinffr 11663  filcon 11665  limfilcf 11683  filmapss 11696  rnelfmlem 11698  fclusss 11723  fcluscf 11724  fcluscnplem 11729  fcluscomp 11733  filnetlem4 11766  uptx 11978  phtpcer 12104

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011

Copyright terms: Public domain