Metamath Proof Explorer

Theorem elwf

Description: An element of a well-founded set is well-founded. (Contributed by BTernaryTau, 30-Dec-2025)

Ref Expression
Assertion elwf 
|- ( ( A e. U. ( R1 " On ) /\ B e. A ) -> B e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( B e. A -> B C_ U. A )
2 uniwf 
 |-  ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) )
3 sswf 
 |-  ( ( U. A e. U. ( R1 " On ) /\ B C_ U. A ) -> B e. U. ( R1 " On ) )
4 2 3 sylanb 
 |-  ( ( A e. U. ( R1 " On ) /\ B C_ U. A ) -> B e. U. ( R1 " On ) )
5 1 4 sylan2 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. A ) -> B e. U. ( R1 " On ) )