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  7954  distrlem5pru  7955  mulrid  8324  cnegex  8506  recexap  8984  creur  9292  creui  9293  cju  9294  elz2  9721  qre  10035  qaddcl  10045  qnegcl  10046  qmulcl  10047  qreccl  10052  elpqb  10061  fundm2domnop0  11316  replim  11640  prodmodc  12364  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  qredeu  12894  pythagtriplem1  13067  pcz  13134  4sqlem1  13190  4sqlem2  13191  4sqlem4  13194  mul4sq  13196  txuni2  15448  blssioo  15745  tgioo  15746  elply  15926  2sqlem2  16400  mul2sq  16401  2sqlem7  16406  upgredgpr  16556