![]() |
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 3193 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) | |
2 | 1 | r2exlem 3141 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∃wex 1776 ∈ wcel 2106 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-ral 3060 df-rex 3069 |
This theorem is referenced by: r3ex 3196 reeanlem 3226 elxp2 5713 elinxp 6039 rnoprab2 7538 elrnmpores 7571 oeeu 8640 omxpenlem 9112 axcnre 11202 hash2prb 14508 hashle2prv 14514 pmtrrn2 19493 fsumvma 27272 umgredg 29170 fusgr2wsp2nb 30363 spanuni 31573 5oalem7 31689 3oalem3 31693 trsp2cyc 33126 fmla0xp 35368 elfuns 35897 ellines 36134 dalem20 39676 diblsmopel 41154 iunrelexpuztr 43709 sprssspr 47406 prprelb 47441 |
Copyright terms: Public domain | W3C validator |