Metamath Proof Explorer

Theorem abbi1dv

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994) (Proof shortened by Wolf Lammen, 16-Nov-2019)

Ref Expression
Hypothesis abbi1dv.1 
|- ( ph -> ( ps <-> x e. A ) )
Assertion abbi1dv 
|- ( ph -> { x | ps } = A )

Proof

Step Hyp Ref Expression
1 abbi1dv.1 
 |-  ( ph -> ( ps <-> x e. A ) )
2 1 bicomd 
 |-  ( ph -> ( x e. A <-> ps ) )
3 2 abbi2dv 
 |-  ( ph -> A = { x | ps } )
4 3 eqcomd 
 |-  ( ph -> { x | ps } = A )