Theorem rexlimivv 2600

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  opelxp  4658  f1o2ndf1  6231  xpdom2  6833  distrlem5prl  7587  distrlem5pru  7588  mulrid  7956  cnegex  8137  recexap  8612  creur  8918  creui  8919  cju  8920  elz2  9326  qre  9627  qaddcl  9637  qnegcl  9638  qmulcl  9639  qreccl  9644  elpqb  9651  replim  10870  prodmodc  11588  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  qredeu  12099  pythagtriplem1  12267  pcz  12333  4sqlem1  12388  4sqlem2  12389  4sqlem4  12392  mul4sq  12394  txuni2  13841  blssioo  14130  tgioo  14131  2sqlem2  14547  mul2sq  14548  2sqlem7  14553