Theorem abeq1

Description: Equality of a class variable and a class abstraction. Commuted form of abeq2 . (Contributed by NM, 20-Aug-1993)

	Ref	Expression
Assertion	abeq1	|- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) )

Proof

Step	Hyp	Ref	Expression
1		abeq2	|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
2		eqcom	|- ( { x | ph } = A <-> A = { x | ph } )
3		bicom	|- ( ( ph <-> x e. A ) <-> ( x e. A <-> ph ) )
4	3	albii	|- ( A. x ( ph <-> x e. A ) <-> A. x ( x e. A <-> ph ) )
5	1 2 4	3bitr4i	|- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) )