Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > moeq | Structured version Visualization version GIF version |
Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.) |
Ref | Expression |
---|---|
moeq | ⊢ ∃*𝑥 𝑥 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isset 3207 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
2 | eueq 3378 | . . 3 ⊢ (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | sylbb1 227 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴) |
4 | df-mo 2475 | . 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴)) | |
5 | 3, 4 | mpbir 221 | 1 ⊢ ∃*𝑥 𝑥 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ∃!weu 2470 ∃*wmo 2471 Vcvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 |
This theorem is referenced by: mosub 3384 euxfr2 3391 reueq 3404 rmoeq 3405 sndisj 4644 disjxsn 4646 reusv1OLD 4867 reuxfr2d 4891 funopabeq 5924 funcnvsn 5936 fvmptg 6280 fvopab6 6310 ovmpt4g 6783 ov3 6797 ov6g 6798 oprabex3 7157 1stconst 7265 2ndconst 7266 iunmapdisj 8846 axaddf 9966 axmulf 9967 joinfval 17001 joinval 17005 meetfval 17015 meetval 17019 reuxfr3d 29329 abrexdom2jm 29346 abrexdom2 33526 |
Copyright terms: Public domain | W3C validator |