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 3203 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) | |
2 | 1 | r2exlem 3304 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ∧ wa 398 ∃wex 1780 ∈ wcel 2114 ∃wrex 3141 |
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 209 df-an 399 df-ex 1781 df-ral 3145 df-rex 3146 |
This theorem is referenced by: rexcomOLD 3358 reeanlem 3367 elxp2 5581 elinxp 5892 rnoprab2 7260 elrnmpores 7290 oeeu 8231 omxpenlem 8620 axcnre 10588 hash2prb 13833 hashle2prv 13839 pmtrrn2 18590 fsumvma 25791 umgredg 26925 fusgr2wsp2nb 28115 spanuni 29323 5oalem7 29439 3oalem3 29443 trsp2cyc 30767 fmla0xp 32632 elfuns 33378 ellines 33615 dalem20 36831 diblsmopel 38309 iunrelexpuztr 40071 sprssspr 43650 prprelb 43685 |
Copyright terms: Public domain | W3C validator |