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

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  19.21aivv 1287  ax11eq 1363  ax11el 1364  eqrdv 1473  abbi2dv 1578  abbi1dv 1579  hbeqd 1913  hbeld 1914  moeq3 1921  sbcthdv 1947  sbc2or 1958  sbciegf 1960  hbsbc1gd 1983  hbsbcgd 1984  sbc19.20dv 1985  sbcel12g 2011  sbceqdig 2012  csbnestglem 2035  csbnestg 2036  csbnest1g 2037  ssrdv 2070  abssdv 2121  uniiunlem 2132  disjsn 2441  hbopd 2497  uniss 2521  intss 2554  intab 2560  iunss1 2574  ssiun 2592  hbbrd 2659  axsep 2702  ssopab2 2822  onminex 3020  limom 3146  hbimad 3412  cotr 3436  funco 3550  funun 3554  fununi 3563  funcnvuni 3564  hbfvd 3730  fopab2 3823  iunon 3909  iinon 3910  hboprd 3982  funoprabg 4010  2ndconst 4097  erdisj 4286  mapss 4346  pw2en 4446  unifiOLD 4557  fiint 4559  fiintOLD 4560  sucprcreg 4600  aceq3 4733  aceq5 4740  aceq6b 4742  kmlem1 4765  kmlem6 4770  kmlem13 4777  brdom6disj 4805  cfub 4908  cflim 4909  cflecard 4912  1pr 5117  reclem2pr 5157  supexpr 5163  hbnegd 5363  dfuz 6202  tgclt 7624  subtop 7646  indistop 7648  neissex 7738  lpval 7743  opntop 7870  cdrci 10494  homeofval 10516  homcard 10539  qusp 10555  fipfil2 10564  fipfil2OLD 10565  cnfilca 10583  cnfilcaOLD 10584  ismonc 10742

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

Copyright terms: Public domain