Theorem rexlimivv 2654

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 2648	. 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓))
3	2	rexlimiv 2642	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  opelxp  4753  f1o2ndf1  6388  xpdom2  7010  distrlem5prl  7796  distrlem5pru  7797  mulrid  8166  cnegex  8347  recexap  8823  creur  9129  creui  9130  cju  9131  elz2  9541  qre  9849  qaddcl  9859  qnegcl  9860  qmulcl  9861  qreccl  9866  elpqb  9874  fundm2domnop0  11099  replim  11410  prodmodc  12129  odd2np1  12424  opoe  12446  omoe  12447  opeo  12448  omeo  12449  qredeu  12659  pythagtriplem1  12828  pcz  12895  4sqlem1  12951  4sqlem2  12952  4sqlem4  12955  mul4sq  12957  txuni2  14970  blssioo  15267  tgioo  15268  elply  15448  2sqlem2  15834  mul2sq  15835  2sqlem7  15840  upgredgpr  15988