Theorem clel2g

Description: An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993) (Revised by BJ, 12-Feb-2022)

	Ref	Expression
Assertion	clel2g	$$⊢A\in V\to \left(A\in B\leftrightarrow \forall x\left(x=A\to x\in B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢ℲxA\in B$$
2		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
3	1 2	ceqsalg	$$⊢A\in V\to \left(\forall x\left(x=A\to x\in B\right)\leftrightarrow A\in B\right)$$
4	3	bicomd	$$⊢A\in V\to \left(A\in B\leftrightarrow \forall x\left(x=A\to x\in B\right)\right)$$