Metamath Proof Explorer

Theorem bj-pr2ex

Description: Sethood of the second projection. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-pr2ex 
|- ( A e. V -> pr2 A e. _V )

Proof

Step Hyp Ref Expression
1 df-bj-pr2 
 |-  pr2 A = ( 1o Proj A )
2 bj-projex 
 |-  ( A e. V -> ( 1o Proj A ) e. _V )
3 1 2 eqeltrid 
 |-  ( A e. V -> pr2 A e. _V )