Theorem clel4

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

	Ref	Expression
Hypothesis	clel4.1	|- B e. _V
Assertion	clel4	|- ( A e. B <-> A. x ( x = B -> A e. x ) )

Proof

Step	Hyp	Ref	Expression
1		clel4.1	|- B e. _V
2		eleq2	|- ( x = B -> ( A e. x <-> A e. B ) )
3	1 2	ceqsalv	|- ( A. x ( x = B -> A e. x ) <-> A e. B )
4	3	bicomi	|- ( A e. B <-> A. x ( x = B -> A e. x ) )