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 𝐴𝐵
Assertion elexi 𝐴 ∈ V


Step Hyp Ref Expression
1 elexi.1 𝐴𝐵
2 elex ( 𝐴𝐵𝐴 ∈ V )
3 1 2 ax-mp 𝐴 ∈ V