Metamath Proof Explorer


Theorem madeun

Description: The made set is the union of the old set and the new set. (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Assertion madeun MA=OldANA

Proof

Step Hyp Ref Expression
1 newval NA=MAOldA
2 1 uneq2i OldANA=OldAMAOldA
3 oldssmade OldAMA
4 undif OldAMAOldAMAOldA=MA
5 3 4 mpbi OldAMAOldA=MA
6 2 5 eqtr2i MA=OldANA