Theorem clel2g

Description: Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993) Strengthen from sethood hypothesis to sethood antecedent (Revised by BJ, 12-Feb-2022) Avoid ax-12 . (Revised by BJ, 1-Sep-2024)

	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		elisset	$$⊢A\in V\to \exists xx=A$$
2		biimt	$$⊢\exists xx=A\to \left(A\in B\leftrightarrow \left(\exists xx=A\to A\in B\right)\right)$$
3	1 2	syl	$$⊢A\in V\to \left(A\in B\leftrightarrow \left(\exists xx=A\to A\in B\right)\right)$$
4		19.23v	$$⊢\forall x\left(x=A\to A\in B\right)\leftrightarrow \left(\exists xx=A\to A\in B\right)$$
5		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
6	5	bicomd	$$⊢x=A\to \left(A\in B\leftrightarrow x\in B\right)$$
7	6	pm5.74i	$$⊢\left(x=A\to A\in B\right)\leftrightarrow \left(x=A\to x\in B\right)$$
8	7	albii	$$⊢\forall x\left(x=A\to A\in B\right)\leftrightarrow \forall x\left(x=A\to x\in B\right)$$
9	4 8	bitr3i	$$⊢\left(\exists xx=A\to A\in B\right)\leftrightarrow \forall x\left(x=A\to x\in B\right)$$
10	3 9	bitrdi	$$⊢A\in V\to \left(A\in B\leftrightarrow \forall x\left(x=A\to x\in B\right)\right)$$