Metamath Proof Explorer

Theorem elex

Description: If a class is a member of another class, then it is a set. Theorem 6.12 of Quine p. 44. (Contributed by NM, 26-May-1993) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Assertion elex A B A V


Step Hyp Ref Expression
1 exsimpl x x = A x B x x = A
2 dfclel A B x x = A x B
3 isset A V x x = A
4 1 2 3 3imtr4i A B A V