Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993) Avoid ax-11 . (Revised by Wolf Lammen, 6-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | abbi2i.1 | |- ( x e. A <-> ph ) |
|
| Assertion | abbi2i | |- A = { x | ph } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abbi2i.1 | |- ( x e. A <-> ph ) |
|
| 2 | 1 | a1i | |- ( T. -> ( x e. A <-> ph ) ) |
| 3 | 2 | abbi2dv | |- ( T. -> A = { x | ph } ) |
| 4 | 3 | mptru | |- A = { x | ph } |