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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | newval | |
|
2 | 1 | uneq2i | |
3 | oldssmade | |
|
4 | undif | |
|
5 | 3 4 | mpbi | |
6 | 2 5 | eqtr2i | |