Theorem rexlimivv 2630

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  opelxp  4713  f1o2ndf1  6327  xpdom2  6941  distrlem5prl  7719  distrlem5pru  7720  mulrid  8089  cnegex  8270  recexap  8746  creur  9052  creui  9053  cju  9054  elz2  9464  qre  9766  qaddcl  9776  qnegcl  9777  qmulcl  9778  qreccl  9783  elpqb  9791  fundm2domnop0  11012  replim  11245  prodmodc  11964  odd2np1  12259  opoe  12281  omoe  12282  opeo  12283  omeo  12284  qredeu  12494  pythagtriplem1  12663  pcz  12730  4sqlem1  12786  4sqlem2  12787  4sqlem4  12790  mul4sq  12792  txuni2  14803  blssioo  15100  tgioo  15101  elply  15281  2sqlem2  15667  mul2sq  15668  2sqlem7  15673