Metamath Proof Explorer


Theorem onelssi

Description: A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994)

Ref Expression
Hypothesis on.1 A On
Assertion onelssi B A B A

Proof

Step Hyp Ref Expression
1 on.1 A On
2 onelss A On B A B A
3 1 2 ax-mp B A B A