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 Old B A M B

Proof

Step Hyp Ref Expression
1 oldssmade Old B M B
2 1 sseli A Old B A M B