Metamath Proof Explorer


Theorem bj-pr2un

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

Ref Expression
Assertion bj-pr2un pr2AB=pr2Apr2B

Proof

Step Hyp Ref Expression
1 bj-projun 1𝑜ProjAB=1𝑜ProjA1𝑜ProjB
2 df-bj-pr2 pr2AB=1𝑜ProjAB
3 df-bj-pr2 pr2A=1𝑜ProjA
4 df-bj-pr2 pr2B=1𝑜ProjB
5 3 4 uneq12i pr2Apr2B=1𝑜ProjA1𝑜ProjB
6 1 2 5 3eqtr4i pr2AB=pr2Apr2B