Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995) Shorten combined proofs of moeq and eueq . (Proof shortened by BJ, 24-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | moeq | |- E* x x = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqtr3 | |- ( ( x = A /\ y = A ) -> x = y ) |
|
| 2 | 1 | gen2 | |- A. x A. y ( ( x = A /\ y = A ) -> x = y ) |
| 3 | eqeq1 | |- ( x = y -> ( x = A <-> y = A ) ) |
|
| 4 | 3 | mo4 | |- ( E* x x = A <-> A. x A. y ( ( x = A /\ y = A ) -> x = y ) ) |
| 5 | 2 4 | mpbir | |- E* x x = A |