Metamath Proof Explorer


Theorem elexi

Description: If a class is a member of another class, then it is a set. Inference associated with elex . (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis elexi.1
|- A e. B
Assertion elexi
|- A e. _V

Proof

Step Hyp Ref Expression
1 elexi.1
 |-  A e. B
2 elex
 |-  ( A e. B -> A e. _V )
3 1 2 ax-mp
 |-  A e. _V