Theorem rexlimivv 2494

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   E.wrex 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365

This theorem is referenced by:  opelxp  4467  f1o2ndf1  5993  xpdom2  6547  distrlem5prl  7145  distrlem5pru  7146  mulid1  7485  cnegex  7660  recexap  8122  creur  8419  creui  8420  cju  8421  elz2  8818  qre  9110  qaddcl  9120  qnegcl  9121  qmulcl  9122  qreccl  9127  replim  10293  odd2np1  11151  opoe  11173  omoe  11174  opeo  11175  omeo  11176  qredeu  11357