Metamath Proof Explorer

Theorem oldmade

Description: An element of an old set is an element of a made set. (Contributed by Scott Fenton, 27-Feb-2026)

Ref Expression
Assertion oldmade 
|- ( A e. ( _Old ` B ) -> A e. ( _Made ` B ) )

Proof

Step Hyp Ref Expression
1 oldssmade 
 |-  ( _Old ` B ) C_ ( _Made ` B )
2 1 sseli 
 |-  ( A e. ( _Old ` B ) -> A e. ( _Made ` B ) )