Theorem rexlimivv 2666

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∃wrex 2521

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  opelxp  4779  f1o2ndf1  6424  xpdom2  7082  distrlem5prl  7901  distrlem5pru  7902  mulrid  8271  cnegex  8451  recexap  8927  creur  9233  creui  9234  cju  9235  elz2  9649  qre  9957  qaddcl  9967  qnegcl  9968  qmulcl  9969  qreccl  9974  elpqb  9982  fundm2domnop0  11220  replim  11544  prodmodc  12264  odd2np1  12559  opoe  12581  omoe  12582  opeo  12583  omeo  12584  qredeu  12794  pythagtriplem1  12963  pcz  13030  4sqlem1  13086  4sqlem2  13087  4sqlem4  13090  mul4sq  13092  txuni2  15121  blssioo  15418  tgioo  15419  elply  15599  2sqlem2  15988  mul2sq  15989  2sqlem7  15994  upgredgpr  16144