Theorem r2ex 3208

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 3086	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑))
2	1	r2exlem 3206	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 197   ∧ wa 384  ∃wex 1874   ∈ wcel 2155  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061

This theorem is referenced by:  reean  3253  elxp2  5303  elinxp  5611  rnoprab2  6946  elrnmpt2res  6976  oeeu  7892  omxpenlem  8272  axcnre  10242  hash2prb  13460  hashle2prv  13466  pmtrrn2  18157  fsumvma  25243  umgredg  26325  fusgr2wsp2nb  27635  spanuni  28880  5oalem7  28996  3oalem3  29000  elfuns  32487  ellines  32724  cnfinltrel  33695  dalem20  35670  diblsmopel  37148  iunrelexpuztr  38710  sprssspr  42424