Theorem rexlimivv 2657

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2512

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 2516  df-rex 2517

This theorem is referenced by:  opelxp  4761  f1o2ndf1  6402  xpdom2  7058  distrlem5prl  7866  distrlem5pru  7867  mulrid  8236  cnegex  8416  recexap  8892  creur  9198  creui  9199  cju  9200  elz2  9612  qre  9920  qaddcl  9930  qnegcl  9931  qmulcl  9932  qreccl  9937  elpqb  9945  fundm2domnop0  11175  replim  11499  prodmodc  12219  odd2np1  12514  opoe  12536  omoe  12537  opeo  12538  omeo  12539  qredeu  12749  pythagtriplem1  12918  pcz  12985  4sqlem1  13041  4sqlem2  13042  4sqlem4  13045  mul4sq  13047  txuni2  15067  blssioo  15364  tgioo  15365  elply  15545  2sqlem2  15934  mul2sq  15935  2sqlem7  15940  upgredgpr  16090