Theorem eqabcdv

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	eqabcdv.1	|- ( ph -> ( ps <-> x e. A ) )
Assertion	eqabcdv	|- ( ph -> { x | ps } = A )

Proof

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