Metamath Proof Explorer

Theorem ordfr

Description: Membership is well-founded on an ordinal class. In other words, an ordinal class is well-founded. (Contributed by NM, 22-Apr-1994)

Ref Expression
Assertion ordfr 
|- ( Ord A -> _E Fr A )

Proof

Step Hyp Ref Expression
1 ordwe 
 |-  ( Ord A -> _E We A )
2 wefr 
 |-  ( _E We A -> _E Fr A )
3 1 2 syl 
 |-  ( Ord A -> _E Fr A )