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	Could not format assertion : No typesetting found for |- ( _Made ` A ) = ( ( _Old ` A ) u. ( _New ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		newval	Could not format ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) : No typesetting found for |- ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) with typecode |-
2	1	uneq2i	Could not format ( ( _Old ` A ) u. ( _New ` A ) ) = ( ( _Old ` A ) u. ( ( _Made ` A ) \ ( _Old ` A ) ) ) : No typesetting found for |- ( ( _Old ` A ) u. ( _New ` A ) ) = ( ( _Old ` A ) u. ( ( _Made ` A ) \ ( _Old ` A ) ) ) with typecode |-
3		oldssmade	Could not format ( _Old ` A ) C_ ( _Made ` A ) : No typesetting found for |- ( _Old ` A ) C_ ( _Made ` A ) with typecode |-
4		undif	Could not format ( ( _Old ` A ) C_ ( _Made ` A ) <-> ( ( _Old ` A ) u. ( ( _Made ` A ) \ ( _Old ` A ) ) ) = ( _Made ` A ) ) : No typesetting found for |- ( ( _Old ` A ) C_ ( _Made ` A ) <-> ( ( _Old ` A ) u. ( ( _Made ` A ) \ ( _Old ` A ) ) ) = ( _Made ` A ) ) with typecode |-
5	3 4	mpbi	Could not format ( ( _Old ` A ) u. ( ( _Made ` A ) \ ( _Old ` A ) ) ) = ( _Made ` A ) : No typesetting found for |- ( ( _Old ` A ) u. ( ( _Made ` A ) \ ( _Old ` A ) ) ) = ( _Made ` A ) with typecode |-
6	2 5	eqtr2i	Could not format ( _Made ` A ) = ( ( _Old ` A ) u. ( _New ` A ) ) : No typesetting found for |- ( _Made ` A ) = ( ( _Old ` A ) u. ( _New ` A ) ) with typecode |-