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 |) = ( { (/) } X. tag A )
2		bj-pr1eq	|- ( (| A |) = ( { (/) } X. tag A ) -> pr1 (| A |) = pr1 ( { (/) } X. tag A ) )
3	1 2	ax-mp	|- pr1 (| A |) = pr1 ( { (/) } X. tag A )
4		bj-pr1val	|- pr1 ( { (/) } X. tag A ) = if ( (/) = (/) , A , (/) )
5		eqid	|- (/) = (/)
6	5	iftruei	|- if ( (/) = (/) , A , (/) ) = A
7	3 4 6	3eqtri	|- pr1 (| A |) = A