![]() |
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 3144 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3063 df-rex 3072 |
This theorem is referenced by: reeanlem 3226 elxp2 5701 elinxp 6020 rnoprab2 7513 elrnmpores 7546 oeeu 8603 omxpenlem 9073 axcnre 11159 hash2prb 14433 hashle2prv 14439 pmtrrn2 19328 fsumvma 26716 umgredg 28398 fusgr2wsp2nb 29587 spanuni 30797 5oalem7 30913 3oalem3 30917 trsp2cyc 32282 fmla0xp 34374 elfuns 34887 ellines 35124 dalem20 38564 diblsmopel 40042 iunrelexpuztr 42470 sprssspr 46149 prprelb 46184 |
Copyright terms: Public domain | W3C validator |