| 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 3713 and eueq 3714. (Proof shortened by BJ, 24-Sep-2022.) |
| Ref | Expression |
|---|---|
| moeq | ⊢ ∃*𝑥 𝑥 = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqtr3 2763 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦) | |
| 2 | 1 | gen2 1796 | . 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦) |
| 3 | eqeq1 2741 | . . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) | |
| 4 | 3 | mo4 2566 | . 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)) |
| 5 | 2, 4 | mpbir 231 | 1 ⊢ ∃*𝑥 𝑥 = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∀wal 1538 = wceq 1540 ∃*wmo 2538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-mo 2540 df-cleq 2729 |
| This theorem is referenced by: eueq 3714 mosub 3719 euxfr2w 3726 euxfr2 3728 reueq 3743 rmoeq 3744 reuxfrd 3754 sndisj 5135 disjxsn 5137 funopabeq 6602 funcnvsn 6616 fvmptg 7014 fvopab6 7050 mpofun 7557 ovmpt4g 7580 ov3 7596 ov6g 7597 abrexexg 7985 oprabex3 8002 1stconst 8125 2ndconst 8126 iunmapdisj 10063 axaddf 11185 axmulf 11186 joinfval 18418 joinval 18422 meetfval 18432 meetval 18436 reuxfrdf 32510 abrexdom2jm 32527 abrexdom2 37738 tfsconcatlem 43349 |
| Copyright terms: Public domain | W3C validator |