Theorem r2ex 3196

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071

This theorem is referenced by:  r3ex  3198  reeanlem  3228  elxp2  5709  elinxp  6037  rnoprab2  7539  elrnmpores  7571  oeeu  8641  omxpenlem  9113  axcnre  11204  hash2prb  14511  hashle2prv  14517  pmtrrn2  19478  fsumvma  27257  umgredg  29155  fusgr2wsp2nb  30353  spanuni  31563  5oalem7  31679  3oalem3  31683  trsp2cyc  33143  fmla0xp  35388  elfuns  35916  ellines  36153  dalem20  39695  diblsmopel  41173  iunrelexpuztr  43732  sprssspr  47468  prprelb  47503