Metamath Proof Explorer


Theorem bj-pr1ex

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

Ref Expression
Assertion bj-pr1ex ( 𝐴𝑉 → pr1 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 df-bj-pr1 pr1 𝐴 = ( ∅ Proj 𝐴 )
2 bj-projex ( 𝐴𝑉 → ( ∅ Proj 𝐴 ) ∈ V )
3 1 2 eqeltrid ( 𝐴𝑉 → pr1 𝐴 ∈ V )