Theorem bj-pr2un

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

	Ref	Expression
Assertion	bj-pr2un	|- pr2 ( A u. B ) = ( pr2 A u. pr2 B )

Proof

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