Theorem r2ex 3222

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399  ∃wex 1787   ∈ wcel 2110  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  reeanlem  3277  elxp2  5575  elinxp  5889  rnoprab2  7315  elrnmpores  7347  oeeu  8331  omxpenlem  8746  axcnre  10778  hash2prb  14038  hashle2prv  14044  pmtrrn2  18852  fsumvma  26094  umgredg  27229  fusgr2wsp2nb  28417  spanuni  29625  5oalem7  29741  3oalem3  29745  trsp2cyc  31109  fmla0xp  33058  elfuns  33954  ellines  34191  dalem20  37444  diblsmopel  38922  iunrelexpuztr  41004  sprssspr  44606  prprelb  44641