Theorem bj-pr1un

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

	Ref	Expression
Assertion	bj-pr1un	|- pr1 ( A u. B ) = ( pr1 A u. pr1 B )

Proof

Step	Hyp	Ref	Expression
1		bj-projun	|- ( (/) Proj ( A u. B ) ) = ( ( (/) Proj A ) u. ( (/) Proj B ) )
2		df-bj-pr1	|- pr1 ( A u. B ) = ( (/) Proj ( A u. B ) )
3		df-bj-pr1	|- pr1 A = ( (/) Proj A )
4		df-bj-pr1	|- pr1 B = ( (/) Proj B )
5	3 4	uneq12i	|- ( pr1 A u. pr1 B ) = ( ( (/) Proj A ) u. ( (/) Proj B ) )
6	1 2 5	3eqtr4i	|- pr1 ( A u. B ) = ( pr1 A u. pr1 B )