Theorem rexlimivv 2666

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  opelxp  4778  f1o2ndf1  6423  xpdom2  7081  distrlem5prl  7900  distrlem5pru  7901  mulrid  8270  cnegex  8450  recexap  8926  creur  9232  creui  9233  cju  9234  elz2  9648  qre  9956  qaddcl  9966  qnegcl  9967  qmulcl  9968  qreccl  9973  elpqb  9981  fundm2domnop0  11216  replim  11540  prodmodc  12260  odd2np1  12555  opoe  12577  omoe  12578  opeo  12579  omeo  12580  qredeu  12790  pythagtriplem1  12959  pcz  13026  4sqlem1  13082  4sqlem2  13083  4sqlem4  13086  mul4sq  13088  txuni2  15113  blssioo  15410  tgioo  15411  elply  15591  2sqlem2  15980  mul2sq  15981  2sqlem7  15986  upgredgpr  16136