Theorem r2ex 3170

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  r3ex  3172  reeanlem  3204  elxp2  5643  elinxp  5972  rnoprab2  7458  elrnmpores  7490  oeeu  8524  omxpenlem  8998  axcnre  11062  hash2prb  14381  hashle2prv  14387  pmtrrn2  19374  fsumvma  27152  umgredg  29118  fusgr2wsp2nb  30316  spanuni  31526  5oalem7  31642  3oalem3  31646  trsp2cyc  33099  fmla0xp  35448  elfuns  35978  ellines  36217  dalem20  39812  diblsmopel  41290  iunrelexpuztr  43836  sprssspr  47605  prprelb  47640