![]() |
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 3191 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) | |
2 | 1 | r2exlem 3140 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 396 ∃wex 1781 ∈ wcel 2106 ∃wrex 3073 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-ral 3065 df-rex 3074 |
This theorem is referenced by: reeanlem 3216 elxp2 5657 elinxp 5975 rnoprab2 7460 elrnmpores 7492 oeeu 8549 omxpenlem 9016 axcnre 11099 hash2prb 14370 hashle2prv 14376 pmtrrn2 19240 fsumvma 26559 umgredg 28036 fusgr2wsp2nb 29225 spanuni 30433 5oalem7 30549 3oalem3 30553 trsp2cyc 31916 fmla0xp 33917 elfuns 34490 ellines 34727 dalem20 38146 diblsmopel 39624 iunrelexpuztr 41972 sprssspr 45644 prprelb 45679 |
Copyright terms: Public domain | W3C validator |