|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > r2ex | Structured version Visualization version GIF version | ||
| Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.) | 
| Ref | Expression | 
|---|---|
| r2ex | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | r2al 3195 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) | |
| 2 | 1 | r2exlem 3143 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | 
| Colors of variables: wff setvar class | 
| 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 | 
| Copyright terms: Public domain | W3C validator |