Theorem r2ex 3200

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  r3ex  3202  reeanlem  3234  elxp2  5675  elinxp  6010  rnoprab2  7518  elrnmpores  7550  oeeu  8596  omxpenlem  9081  axcnre  11230  hash2prb  14597  hashle2prv  14603  pmtrrn2  19654  fsumvma  27522  umgredg  29698  fusgr2wsp2nb  30917  spanuni  32128  5oalem7  32244  3oalem3  32248  trsp2cyc  33666  fmla0xp  36117  elfuns  36647  ellines  36887  dalem20  40718  diblsmopel  42196  iunrelexpuztr  44678  sprssspr  48507  prprelb  48542