Metamath Proof Explorer

Theorem dfclel

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

Ref Expression
Assertion dfclel A B x x = A x B


Step Hyp Ref Expression
1 cleljust y z u u = y u z
2 cleljust t t v v = t v t
3 1 2 df-clel A B x x = A x B