Theorem rexlimivv 2656

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  opelxp  4755  f1o2ndf1  6392  xpdom2  7014  distrlem5prl  7805  distrlem5pru  7806  mulrid  8175  cnegex  8356  recexap  8832  creur  9138  creui  9139  cju  9140  elz2  9550  qre  9858  qaddcl  9868  qnegcl  9869  qmulcl  9870  qreccl  9875  elpqb  9883  fundm2domnop0  11108  replim  11419  prodmodc  12138  odd2np1  12433  opoe  12455  omoe  12456  opeo  12457  omeo  12458  qredeu  12668  pythagtriplem1  12837  pcz  12904  4sqlem1  12960  4sqlem2  12961  4sqlem4  12964  mul4sq  12966  txuni2  14979  blssioo  15276  tgioo  15277  elply  15457  2sqlem2  15843  mul2sq  15844  2sqlem7  15849  upgredgpr  15999