Theorem reximdai 2901

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)

Hypotheses

Ref	Expression
reximdai.1	|- F/ x ph
reximdai.2	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

Ref	Expression
reximdai	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Proof of Theorem reximdai

Step	Hyp	Ref	Expression
1		reximdai.1	. . 3 |- F/ x ph
2		reximdai.2	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	1, 2	ralrimi 2832	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
4		rexim 2897	. 2 |- ( A. x e. A ( ps -> ch ) -> ( E. x e. A ps -> E. x e. A ch ) )
5	3, 4	syl 17	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   F/wnf 1663   e. wcel 1870   A.wral 2782   E.wrex 2783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2787  df-rex 2788

This theorem is referenced by:  reximdvaiOLD  2905  tz7.49  7170  hsmexlem2  8855  acunirnmpt2  28102  acunirnmpt2f  28103  locfinreflem  28506  cmpcref  28516  indexdom  31764  filbcmb  31770  cdlemefr29exN  33677  disjrnmpt2  37085  fompt  37089  disjinfi  37090  supxrge  37169  suplesup  37170  infrglbOLD  37240  limsupre  37292  limsupreOLD  37293  stoweidlem31  37460  stoweidlem34  37463  fourierdlem73  37610  sge0pnffigt  37771  sge0ltfirp  37775  iundjiun  37806  2reurex  37992