Theorem rexlimivv 2593

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

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

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  opelxp  4641  f1o2ndf1  6207  xpdom2  6809  distrlem5prl  7548  distrlem5pru  7549  mulid1  7917  cnegex  8097  recexap  8571  creur  8875  creui  8876  cju  8877  elz2  9283  qre  9584  qaddcl  9594  qnegcl  9595  qmulcl  9596  qreccl  9601  elpqb  9608  replim  10823  prodmodc  11541  odd2np1  11832  opoe  11854  omoe  11855  opeo  11856  omeo  11857  qredeu  12051  pythagtriplem1  12219  pcz  12285  4sqlem1  12340  4sqlem2  12341  4sqlem4  12344  mul4sq  12346  txuni2  13050  blssioo  13339  tgioo  13340  2sqlem2  13745  mul2sq  13746  2sqlem7  13751