Theorem rexlimivv 2588

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  ∃wrex 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448  df-rex 2449

This theorem is referenced by:  opelxp  4633  f1o2ndf1  6192  xpdom2  6793  distrlem5prl  7523  distrlem5pru  7524  mulid1  7892  cnegex  8072  recexap  8546  creur  8850  creui  8851  cju  8852  elz2  9258  qre  9559  qaddcl  9569  qnegcl  9570  qmulcl  9571  qreccl  9576  elpqb  9583  replim  10797  prodmodc  11515  odd2np1  11806  opoe  11828  omoe  11829  opeo  11830  omeo  11831  qredeu  12025  pythagtriplem1  12193  pcz  12259  4sqlem1  12314  4sqlem2  12315  4sqlem4  12318  mul4sq  12320  txuni2  12856  blssioo  13145  tgioo  13146  2sqlem2  13551  mul2sq  13552  2sqlem7  13557