Theorem r2ex 3186

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 394  ∃wex 1773   ∈ wcel 2098  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-ral 3052  df-rex 3061

This theorem is referenced by:  reeanlem  3216  elxp2  5701  elinxp  6023  rnoprab2  7523  elrnmpores  7557  oeeu  8622  omxpenlem  9096  axcnre  11187  hash2prb  14465  hashle2prv  14471  pmtrrn2  19419  fsumvma  27176  umgredg  29007  fusgr2wsp2nb  30200  spanuni  31410  5oalem7  31526  3oalem3  31530  trsp2cyc  32901  fmla0xp  35063  elfuns  35581  ellines  35818  dalem20  39235  diblsmopel  40713  iunrelexpuztr  43214  sprssspr  46884  prprelb  46919