Theorem rexlimivv 2629

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 2623	. 2 |- ( x e. A -> ( E. y e. B ph -> ps ) )
3	2	rexlimiv 2617	1 |- ( E. x e. A E. y e. B ph -> ps )

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  opelxp  4706  f1o2ndf1  6316  xpdom2  6928  distrlem5prl  7701  distrlem5pru  7702  mulrid  8071  cnegex  8252  recexap  8728  creur  9034  creui  9035  cju  9036  elz2  9446  qre  9748  qaddcl  9758  qnegcl  9759  qmulcl  9760  qreccl  9765  elpqb  9773  fundm2domnop0  10992  replim  11203  prodmodc  11922  odd2np1  12217  opoe  12239  omoe  12240  opeo  12241  omeo  12242  qredeu  12452  pythagtriplem1  12621  pcz  12688  4sqlem1  12744  4sqlem2  12745  4sqlem4  12748  mul4sq  12750  txuni2  14761  blssioo  15058  tgioo  15059  elply  15239  2sqlem2  15625  mul2sq  15626  2sqlem7  15631