Theorem r2ex 3201

Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.)

Assertion

Ref	Expression
r2ex	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝐴(𝑥)   𝐵(𝑥, 𝑦)

Proof of Theorem r2ex

Step	Hyp	Ref	Expression
1		r2al 3200	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑))
2	1	r2exlem 3153	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 400  ∃wex 1808   ∈ wcel 2142  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-ral 3079  df-rex 3089

This theorem is used by:  r3ex  3203  reeanlem  3235  elxp2  5684  elinxp  6017  rnoprab2  7518  elrnmpores  7550  oeeu  8587  omxpenlem  9064  axcnre  11155  hash2prb  14516  hashle2prv  14522  pmtrrn2  19536  fsumvma  27388  umgredg  29499  fusgr2wsp2nb  30696  spanuni  31907  5oalem7  32023  3oalem3  32027  trsp2cyc  33452  fmla0xp  35883  elfuns  36413  ellines  36652  dalem20  40495  diblsmopel  41973  iunrelexpuztr  44473  sprssspr  48258  prprelb  48293