Theorem rexlimivv 2628

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2175  ∃wrex 2484

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  opelxp  4703  f1o2ndf1  6304  xpdom2  6908  distrlem5prl  7681  distrlem5pru  7682  mulrid  8051  cnegex  8232  recexap  8708  creur  9014  creui  9015  cju  9016  elz2  9426  qre  9728  qaddcl  9738  qnegcl  9739  qmulcl  9740  qreccl  9745  elpqb  9753  replim  11089  prodmodc  11808  odd2np1  12103  opoe  12125  omoe  12126  opeo  12127  omeo  12128  qredeu  12338  pythagtriplem1  12507  pcz  12574  4sqlem1  12630  4sqlem2  12631  4sqlem4  12634  mul4sq  12636  txuni2  14646  blssioo  14943  tgioo  14944  elply  15124  2sqlem2  15510  mul2sq  15511  2sqlem7  15516