Description: Equality of a class variable and a class abstraction (deduction form of abeq2 ). (Contributed by NM, 16-Nov-1995)
Ref | Expression | ||
---|---|---|---|
Hypothesis | abeq2d.1 | |- ( ph -> A = { x | ps } ) |
|
Assertion | abeq2d | |- ( ph -> ( x e. A <-> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeq2d.1 | |- ( ph -> A = { x | ps } ) |
|
2 | 1 | eleq2d | |- ( ph -> ( x e. A <-> x e. { x | ps } ) ) |
3 | abid | |- ( x e. { x | ps } <-> ps ) |
|
4 | 2 3 | bitrdi | |- ( ph -> ( x e. A <-> ps ) ) |