Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993) Avoid ax-12 , based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | abbidv.1 | |- ( ph -> ( ps <-> ch ) ) |
|
| Assertion | abbidv | |- ( ph -> { x | ps } = { x | ch } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abbidv.1 | |- ( ph -> ( ps <-> ch ) ) |
|
| 2 | 1 | alrimiv | |- ( ph -> A. x ( ps <-> ch ) ) |
| 3 | abbi1 | |- ( A. x ( ps <-> ch ) -> { x | ps } = { x | ch } ) |
|
| 4 | 2 3 | syl | |- ( ph -> { x | ps } = { x | ch } ) |