Metamath Proof Explorer

Theorem onelini

Description: An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis on.1 
|- A e. On
Assertion onelini 
|- ( B e. A -> B = ( B i^i A ) )

Proof

Step Hyp Ref Expression
1 on.1 
 |-  A e. On
2 1 onelssi 
 |-  ( B e. A -> B C_ A )
3 dfss 
 |-  ( B C_ A <-> B = ( B i^i A ) )
4 2 3 sylib 
 |-  ( B e. A -> B = ( B i^i A ) )