Theorem rexlimivv 2553

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   E.wrex 2415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419  df-rex 2420

This theorem is referenced by:  opelxp  4564  f1o2ndf1  6118  xpdom2  6718  distrlem5prl  7387  distrlem5pru  7388  mulid1  7756  cnegex  7933  recexap  8407  creur  8710  creui  8711  cju  8712  elz2  9115  qre  9410  qaddcl  9420  qnegcl  9421  qmulcl  9422  qreccl  9427  replim  10624  odd2np1  11559  opoe  11581  omoe  11582  opeo  11583  omeo  11584  qredeu  11767  txuni2  12414  blssioo  12703  tgioo  12704