Theorem bj-pr1un

Description: The first projection preserves unions. (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-pr1un	⊢ pr1 ( 𝐴 ∪ 𝐵 ) = ( pr1 𝐴 ∪ pr1 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bj-projun	⊢ ( ∅ Proj ( 𝐴 ∪ 𝐵 ) ) = ( ( ∅ Proj 𝐴 ) ∪ ( ∅ Proj 𝐵 ) )
2		df-bj-pr1	⊢ pr1 ( 𝐴 ∪ 𝐵 ) = ( ∅ Proj ( 𝐴 ∪ 𝐵 ) )
3		df-bj-pr1	⊢ pr1 𝐴 = ( ∅ Proj 𝐴 )
4		df-bj-pr1	⊢ pr1 𝐵 = ( ∅ Proj 𝐵 )
5	3 4	uneq12i	⊢ ( pr1 𝐴 ∪ pr1 𝐵 ) = ( ( ∅ Proj 𝐴 ) ∪ ( ∅ Proj 𝐵 ) )
6	1 2 5	3eqtr4i	⊢ pr1 ( 𝐴 ∪ 𝐵 ) = ( pr1 𝐴 ∪ pr1 𝐵 )