Theorem clel4g

Description: Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993) Strengthen from sethood hypothesis to sethood antecedent and avoid ax-12 . (Revised by BJ, 1-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elisset	$$⊢B\in V\to \exists xx=B$$
2		biimt	$$⊢\exists xx=B\to \left(A\in B\leftrightarrow \left(\exists xx=B\to A\in B\right)\right)$$
3	1 2	syl	$$⊢B\in V\to \left(A\in B\leftrightarrow \left(\exists xx=B\to A\in B\right)\right)$$
4		19.23v	$$⊢\forall x\left(x=B\to A\in B\right)\leftrightarrow \left(\exists xx=B\to A\in B\right)$$
5	3 4	bitr4di	$$⊢B\in V\to \left(A\in B\leftrightarrow \forall x\left(x=B\to A\in B\right)\right)$$
6		eleq2	$$⊢x=B\to \left(A\in x\leftrightarrow A\in B\right)$$
7	6	bicomd	$$⊢x=B\to \left(A\in B\leftrightarrow A\in x\right)$$
8	7	pm5.74i	$$⊢\left(x=B\to A\in B\right)\leftrightarrow \left(x=B\to A\in x\right)$$
9	8	albii	$$⊢\forall x\left(x=B\to A\in B\right)\leftrightarrow \forall x\left(x=B\to A\in x\right)$$
10	5 9	bitrdi	$$⊢B\in V\to \left(A\in B\leftrightarrow \forall x\left(x=B\to A\in x\right)\right)$$