Theorem elab6g

Description: Membership in a class abstraction. Class version of sb6 . (Contributed by SN, 5-Oct-2024)

	Ref	Expression
Assertion	elab6g	$$⊢A\in V\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢y=A\to \left(y\in \left\{x|\phi \right\}\leftrightarrow A\in \left\{x|\phi \right\}\right)$$
2		eqeq2	$$⊢y=A\to \left(x=y\leftrightarrow x=A\right)$$
3	2	imbi1d	$$⊢y=A\to \left(\left(x=y\to \phi \right)\leftrightarrow \left(x=A\to \phi \right)\right)$$
4	3	albidv	$$⊢y=A\to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
5		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
6		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
7	5 6	bitri	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \forall x\left(x=y\to \phi \right)$$
8	1 4 7	vtoclbg	$$⊢A\in V\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$