Description: A class is a set if and only if there exists a unique set equal to it. (Contributed by NM, 25-Nov-1994) Shorten combined proofs of moeq and eueq . (Proof shortened by BJ, 24-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eueq | |- ( A e. _V <-> E! x x = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | moeq | |- E* x x = A |
|
| 2 | 1 | biantru | |- ( E. x x = A <-> ( E. x x = A /\ E* x x = A ) ) |
| 3 | isset | |- ( A e. _V <-> E. x x = A ) |
|
| 4 | df-eu | |- ( E! x x = A <-> ( E. x x = A /\ E* x x = A ) ) |
|
| 5 | 2 3 4 | 3bitr4i | |- ( A e. _V <-> E! x x = A ) |