Description: Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq , bj-pr22val , bj-pr2ex . (Contributed by BJ, 6-Oct-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | df-bj-pr2 | ⊢ pr2 𝐴 = ( 1o Proj 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cA | ⊢ 𝐴 | |
1 | 0 | bj-cpr2 | ⊢ pr2 𝐴 |
2 | c1o | ⊢ 1o | |
3 | 2 0 | bj-cproj | ⊢ ( 1o Proj 𝐴 ) |
4 | 1 3 | wceq | ⊢ pr2 𝐴 = ( 1o Proj 𝐴 ) |