![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > moeq | Structured version Visualization version GIF version |
Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3613 and eueq 3614. (Proof shortened by BJ, 24-Sep-2022.) |
Ref | Expression |
---|---|
moeq | ⊢ ∃*𝑥 𝑥 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr3 2802 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦) | |
2 | 1 | gen2 1759 | . 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦) |
3 | eqeq1 2783 | . . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) | |
4 | 3 | mo4 2582 | . 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)) |
5 | 2, 4 | mpbir 223 | 1 ⊢ ∃*𝑥 𝑥 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∀wal 1505 = wceq 1507 ∃*wmo 2545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-cleq 2772 |
This theorem is referenced by: eueq 3614 mosub 3619 euxfr2 3626 reueq 3641 rmoeq 3642 reuxfr3d 3652 sndisj 4921 disjxsn 4923 funopabeq 6224 funcnvsn 6237 fvmptg 6593 fvopab6 6626 ovmpt4g 7113 ov3 7127 ov6g 7128 oprabex3 7490 1stconst 7603 2ndconst 7604 iunmapdisj 9243 axaddf 10365 axmulf 10366 joinfval 17469 joinval 17473 meetfval 17483 meetval 17487 abrexdom2jm 30047 abrexdom2 34445 |
Copyright terms: Public domain | W3C validator |