Theorem 19.21aiv 1286

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

Syntax hints:   -> wi 3  A.wal 953

This theorem is referenced by:  19.21aivv 1287  ax11eq 1363  ax11el 1364  eqrdv 1473  abbi2dv 1577  abbi1dv 1578  hbeqd 1911  hbeld 1912  moeq3 1919  sbcthdv 1945  sbc2or 1956  sbciegf 1958  hbsbc1gd 1981  hbsbcgd 1982  sbc19.20dv 1983  sbcel12g 2009  sbceqdig 2010  csbnestglem 2033  csbnestg 2034  csbnest1g 2035  ssrdv 2068  abssdv 2119  uniiunlem 2130  disjsn 2439  hbopd 2495  uniss 2518  intss 2551  intab 2557  iunss1 2571  ssiun 2589  hbbrd 2656  axsep 2699  ssopab2 2819  onminex 3017  limom 3143  hbimad 3409  cotr 3433  funco 3547  funun 3551  fununi 3560  funcnvuni 3561  hbfvd 3727  fopab2 3820  iunon 3906  iinon 3907  hboprd 3979  funoprabg 4007  2ndconst 4094  erdisj 4283  mapss 4343  pw2en 4439  unifi 4545  fiint 4547  sucprcreg 4587  aceq3 4720  aceq5 4727  aceq6b 4729  kmlem1 4752  kmlem6 4757  kmlem13 4764  brdom6disj 4792  cfub 4895  cflim 4896  cflecard 4899  1pr 5104  reclem2pr 5144  supexpr 5150  hbnegd 5350  dfuz 6164  tgclt 7603  subtop 7625  indistop 7627  neissex 7717  lpval 7722  opntop 7853  gelcomplOLD 10410  cdrci 10475  homeofval 10497  homcard 10520  qusp 10524  fipfil2 10533  cnfilca 10545  ismonc 10691

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

Copyright terms: Public domain