![]() |
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 3185 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) | |
2 | 1 | r2exlem 3133 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 394 ∃wex 1774 ∈ wcel 2099 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-ral 3052 df-rex 3061 |
This theorem is referenced by: reeanlem 3216 elxp2 5706 elinxp 6028 rnoprab2 7530 elrnmpores 7564 oeeu 8633 omxpenlem 9111 axcnre 11207 hash2prb 14491 hashle2prv 14497 pmtrrn2 19458 fsumvma 27242 umgredg 29074 fusgr2wsp2nb 30267 spanuni 31477 5oalem7 31593 3oalem3 31597 trsp2cyc 33001 fmla0xp 35211 elfuns 35739 ellines 35976 dalem20 39392 diblsmopel 40870 iunrelexpuztr 43386 sprssspr 47053 prprelb 47088 |
Copyright terms: Public domain | W3C validator |