Theorem bj-pr1un

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

	Ref	Expression
Assertion	bj-pr1un	$$⊢pr1\left(A\cup B\right)=pr1A\cup pr1B$$

Proof

Step	Hyp	Ref	Expression
1		bj-projun	$$⊢\left(\varnothing Proj\left(A\cup B\right)\right)=\left(\varnothing ProjA\right)\cup \left(\varnothing ProjB\right)$$
2		df-bj-pr1	$$⊢pr1\left(A\cup B\right)=\left(\varnothing Proj\left(A\cup B\right)\right)$$
3		df-bj-pr1	$$⊢pr1A=\left(\varnothing ProjA\right)$$
4		df-bj-pr1	$$⊢pr1B=\left(\varnothing ProjB\right)$$
5	3 4	uneq12i	$$⊢pr1A\cup pr1B=\left(\varnothing ProjA\right)\cup \left(\varnothing ProjB\right)$$
6	1 2 5	3eqtr4i	$$⊢pr1\left(A\cup B\right)=pr1A\cup pr1B$$