Metamath Proof Explorer

Theorem bj-pr1ex

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

Ref Expression
Assertion bj-pr1ex 
|- ( A e. V -> pr1 A e. _V )

Proof

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