Theorem rexlimivv 2613

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)

Hypothesis

Ref	Expression
rexlimivv.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓))

Assertion

Ref	Expression
rexlimivv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝑦,𝜓   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimivv

Step	Hyp	Ref	Expression
1		rexlimivv.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓))
2	1	rexlimdva 2607	. 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓))
3	2	rexlimiv 2601	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160  ∃wrex 2469

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 2473  df-rex 2474

This theorem is referenced by:  opelxp  4671  f1o2ndf1  6247  xpdom2  6849  distrlem5prl  7604  distrlem5pru  7605  mulrid  7973  cnegex  8154  recexap  8629  creur  8935  creui  8936  cju  8937  elz2  9343  qre  9644  qaddcl  9654  qnegcl  9655  qmulcl  9656  qreccl  9661  elpqb  9668  replim  10887  prodmodc  11605  odd2np1  11897  opoe  11919  omoe  11920  opeo  11921  omeo  11922  qredeu  12116  pythagtriplem1  12284  pcz  12350  4sqlem1  12405  4sqlem2  12406  4sqlem4  12409  mul4sq  12411  txuni2  14159  blssioo  14448  tgioo  14449  2sqlem2  14865  mul2sq  14866  2sqlem7  14871