Metamath Proof Explorer

Theorem oneluni

Description: An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994)

Ref Expression
Hypothesis on.1 
|- A e. On
Assertion oneluni 
|- ( B e. A -> ( A u. B ) = A )

Proof

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