![]() |
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 3088 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) | |
2 | 1 | r2exlem 3207 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∧ wa 382 ∃wex 1852 ∈ wcel 2145 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-ral 3066 df-rex 3067 |
This theorem is referenced by: reean 3254 elxp2 5273 rnoprab2 6895 elrnmpt2res 6925 oeeu 7841 omxpenlem 8221 axcnre 10191 hash2prb 13456 hashle2prv 13462 pmtrrn2 18087 fsumvma 25159 umgredg 26255 fusgr2wsp2nb 27516 spanuni 28743 5oalem7 28859 3oalem3 28863 elfuns 32359 ellines 32596 cnfinltrel 33578 dalem20 35502 diblsmopel 36981 iunrelexpuztr 38537 sprssspr 42256 |
Copyright terms: Public domain | W3C validator |