![]() |
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 3699 and eueq 3700. (Proof shortened by BJ, 24-Sep-2022.) |
Ref | Expression |
---|---|
moeq | ⊢ ∃*𝑥 𝑥 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr3 2751 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦) | |
2 | 1 | gen2 1790 | . 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦) |
3 | eqeq1 2729 | . . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) | |
4 | 3 | mo4 2554 | . 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)) |
5 | 2, 4 | mpbir 230 | 1 ⊢ ∃*𝑥 𝑥 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∀wal 1531 = wceq 1533 ∃*wmo 2526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-mo 2528 df-cleq 2717 |
This theorem is referenced by: eueq 3700 mosub 3705 euxfr2w 3712 euxfr2 3714 reueq 3729 rmoeq 3730 reuxfrd 3740 sndisj 5140 disjxsn 5142 funopabeq 6590 funcnvsn 6604 fvmptg 7002 fvopab6 7038 mpofun 7544 ovmpt4g 7568 ov3 7584 ov6g 7585 abrexexg 7965 oprabex3 7982 1stconst 8105 2ndconst 8106 iunmapdisj 10048 axaddf 11170 axmulf 11171 joinfval 18368 joinval 18372 meetfval 18382 meetval 18386 reuxfrdf 32367 abrexdom2jm 32381 abrexdom2 37335 tfsconcatlem 42907 |
Copyright terms: Public domain | W3C validator |