Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996) (Proof shortened by Wolf Lammen, 15-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | abeq2i.1 | |- A = { x | ph } |
|
| Assertion | abeq2i | |- ( x e. A <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abeq2i.1 | |- A = { x | ph } |
|
| 2 | 1 | a1i | |- ( T. -> A = { x | ph } ) |
| 3 | 2 | abeq2d | |- ( T. -> ( x e. A <-> ph ) ) |
| 4 | 3 | mptru | |- ( x e. A <-> ph ) |