Theorem djueq12

Description: Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022)

	Ref	Expression
Assertion	djueq12	|- ( ( A = B /\ C = D ) -> ( A |_| C ) = ( B |_| D ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq2	|- ( A = B -> ( { (/) } X. A ) = ( { (/) } X. B ) )
2	1	adantr	|- ( ( A = B /\ C = D ) -> ( { (/) } X. A ) = ( { (/) } X. B ) )
3		xpeq2	|- ( C = D -> ( { 1o } X. C ) = ( { 1o } X. D ) )
4	3	adantl	|- ( ( A = B /\ C = D ) -> ( { 1o } X. C ) = ( { 1o } X. D ) )
5	2 4	uneq12d	|- ( ( A = B /\ C = D ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) = ( ( { (/) } X. B ) u. ( { 1o } X. D ) ) )
6		df-dju	|- ( A |_| C ) = ( ( { (/) } X. A ) u. ( { 1o } X. C ) )
7		df-dju	|- ( B |_| D ) = ( ( { (/) } X. B ) u. ( { 1o } X. D ) )
8	5 6 7	3eqtr4g	|- ( ( A = B /\ C = D ) -> ( A |_| C ) = ( B |_| D ) )