Theorem rexlimivv 2674

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  opelxp  4804  f1o2ndf1  6464  xpdom2  7129  distrlem5prl  7953  distrlem5pru  7954  mulrid  8323  cnegex  8504  recexap  8981  creur  9289  creui  9290  cju  9291  elz2  9716  qre  10025  qaddcl  10035  qnegcl  10036  qmulcl  10037  qreccl  10042  elpqb  10050  fundm2domnop0  11300  replim  11624  prodmodc  12345  odd2np1  12640  opoe  12662  omoe  12663  opeo  12664  omeo  12665  qredeu  12875  pythagtriplem1  13044  pcz  13111  4sqlem1  13167  4sqlem2  13168  4sqlem4  13171  mul4sq  13173  txuni2  15357  blssioo  15654  tgioo  15655  elply  15835  2sqlem2  16234  mul2sq  16235  2sqlem7  16240  upgredgpr  16390