This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abbid

Description: Equivalent wff's yield equal class abstractions (deduction form, with nonfreeness hypothesis). (Contributed by NM, 21-Jun-1993) (Revised by Mario Carneiro, 7-Oct-2016) Avoid ax-10 and ax-11 . (Revised by Wolf Lammen, 6-May-2023)

Ref Expression
Hypotheses abbid.1 
|- F/ x ph
abbid.2 
|- ( ph -> ( ps <-> ch ) )
Assertion abbid 
|- ( ph -> { x | ps } = { x | ch } )

Proof

Step Hyp Ref Expression
1 abbid.1 
 |-  F/ x ph
2 abbid.2 
 |-  ( ph -> ( ps <-> ch ) )
3 1 2 alrimi 
 |-  ( ph -> A. x ( ps <-> ch ) )
4 abbi 
 |-  ( A. x ( ps <-> ch ) -> { x | ps } = { x | ch } )
5 3 4 syl 
 |-  ( ph -> { x | ps } = { x | ch } )