Theorem abeq2d

Description: Equality of a class variable and a class abstraction (deduction form of abeq2 ). (Contributed by NM, 16-Nov-1995)

	Ref	Expression
Hypothesis	abeq2d.1	$$⊢\phi \to A=\left\{x|\psi \right\}$$
Assertion	abeq2d	$$⊢\phi \to \left(x\in A\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abeq2d.1	$$⊢\phi \to A=\left\{x|\psi \right\}$$
2	1	eleq2d	$$⊢\phi \to \left(x\in A\leftrightarrow x\in \left\{x|\psi \right\}\right)$$
3		abid	$$⊢x\in \left\{x|\psi \right\}\leftrightarrow \psi$$
4	2 3	bitrdi	$$⊢\phi \to \left(x\in A\leftrightarrow \psi \right)$$