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

Proof

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