This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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