Metamath Proof Explorer

Theorem dfclel

Description: Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion dfclel 
|- ( A e. B <-> E. x ( x = A /\ x e. B ) )

Proof

Step Hyp Ref Expression
1 cleljust 
 |-  ( y e. z <-> E. u ( u = y /\ u e. z ) )
2 cleljust 
 |-  ( t e. t <-> E. v ( v = t /\ v e. t ) )
3 1 2 df-clel 
 |-  ( A e. B <-> E. x ( x = A /\ x e. B ) )