Theorem rexlimivv 2631

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)

Hypothesis

Ref	Expression
rexlimivv.1	|- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )

Assertion

Ref	Expression
rexlimivv	|- ( E. x e. A E. y e. B ph -> ps )

Distinct variable groups:   x, y, ps   y, A

Allowed substitution hints:   ph( x, y)   A( x)   B( x, y)

Proof of Theorem rexlimivv

Step	Hyp	Ref	Expression
1		rexlimivv.1	. . 3 |- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )
2	1	rexlimdva 2625	. 2 |- ( x e. A -> ( E. y e. B ph -> ps ) )
3	2	rexlimiv 2619	1 |- ( E. x e. A E. y e. B ph -> ps )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178   E.wrex 2487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  opelxp  4723  f1o2ndf1  6337  xpdom2  6951  distrlem5prl  7734  distrlem5pru  7735  mulrid  8104  cnegex  8285  recexap  8761  creur  9067  creui  9068  cju  9069  elz2  9479  qre  9781  qaddcl  9791  qnegcl  9792  qmulcl  9793  qreccl  9798  elpqb  9806  fundm2domnop0  11027  replim  11285  prodmodc  12004  odd2np1  12299  opoe  12321  omoe  12322  opeo  12323  omeo  12324  qredeu  12534  pythagtriplem1  12703  pcz  12770  4sqlem1  12826  4sqlem2  12827  4sqlem4  12830  mul4sq  12832  txuni2  14843  blssioo  15140  tgioo  15141  elply  15321  2sqlem2  15707  mul2sq  15708  2sqlem7  15713  upgredgpr  15853