Theorem abeq2i

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996) (Proof shortened by Wolf Lammen, 15-Nov-2019)

	Ref	Expression
Hypothesis	abeq2i.1	$$⊢A=\left\{x|\phi \right\}$$
Assertion	abeq2i	$$⊢x\in A\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		abeq2i.1	$$⊢A=\left\{x|\phi \right\}$$
2	1	a1i	$$⊢\top \to A=\left\{x|\phi \right\}$$
3	2	abeq2d	$$⊢\top \to \left(x\in A\leftrightarrow \phi \right)$$
4	3	mptru	$$⊢x\in A\leftrightarrow \phi$$