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	$$⊢\left\{x|\phi \right\}=A\leftrightarrow \forall x\left(\phi \leftrightarrow x\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		abeq2	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \phi \right)$$
2		eqcom	$$⊢\left\{x|\phi \right\}=A\leftrightarrow A=\left\{x|\phi \right\}$$
3		bicom	$$⊢\left(\phi \leftrightarrow x\in A\right)\leftrightarrow \left(x\in A\leftrightarrow \phi \right)$$
4	3	albii	$$⊢\forall x\left(\phi \leftrightarrow x\in A\right)\leftrightarrow \forall x\left(x\in A\leftrightarrow \phi \right)$$
5	1 2 4	3bitr4i	$$⊢\left\{x|\phi \right\}=A\leftrightarrow \forall x\left(\phi \leftrightarrow x\in A\right)$$