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