Theorem rexlimivv 2617

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  opelxp  4689  f1o2ndf1  6281  xpdom2  6885  distrlem5prl  7646  distrlem5pru  7647  mulrid  8016  cnegex  8197  recexap  8672  creur  8978  creui  8979  cju  8980  elz2  9388  qre  9690  qaddcl  9700  qnegcl  9701  qmulcl  9702  qreccl  9707  elpqb  9715  replim  11003  prodmodc  11721  odd2np1  12014  opoe  12036  omoe  12037  opeo  12038  omeo  12039  qredeu  12235  pythagtriplem1  12403  pcz  12470  4sqlem1  12526  4sqlem2  12527  4sqlem4  12530  mul4sq  12532  txuni2  14424  blssioo  14713  tgioo  14714  elply  14880  2sqlem2  15202  mul2sq  15203  2sqlem7  15208