Metamath Proof Explorer


Theorem bj-pr11val

Description: Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-pr11val pr1 A = A

Proof

Step Hyp Ref Expression
1 df-bj-1upl A = × tag A
2 bj-pr1eq A = × tag A pr1 A = pr1 × tag A
3 1 2 ax-mp pr1 A = pr1 × tag A
4 bj-pr1val pr1 × tag A = if = A
5 eqid =
6 5 iftruei if = A = A
7 3 4 6 3eqtri pr1 A = A