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 e. V -> ( A e. B <-> A. x ( x = A -> x e. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		elisset	|- ( A e. V -> E. x x = A )
2		biimt	|- ( E. x x = A -> ( A e. B <-> ( E. x x = A -> A e. B ) ) )
3	1 2	syl	|- ( A e. V -> ( A e. B <-> ( E. x x = A -> A e. B ) ) )
4		19.23v	|- ( A. x ( x = A -> A e. B ) <-> ( E. x x = A -> A e. B ) )
5		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
6	5	bicomd	|- ( x = A -> ( A e. B <-> x e. B ) )
7	6	pm5.74i	|- ( ( x = A -> A e. B ) <-> ( x = A -> x e. B ) )
8	7	albii	|- ( A. x ( x = A -> A e. B ) <-> A. x ( x = A -> x e. B ) )
9	4 8	bitr3i	|- ( ( E. x x = A -> A e. B ) <-> A. x ( x = A -> x e. B ) )
10	3 9	bitrdi	|- ( A e. V -> ( A e. B <-> A. x ( x = A -> x e. B ) ) )