Theorem bj-pr1val

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

	Ref	Expression
Assertion	bj-pr1val	$$⊢pr1\left(\left\{A\right\}\times tagB\right)=if\left(A=\varnothing ,B,\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-pr1	$$⊢pr1\left(\left\{A\right\}\times tagB\right)=\left(\varnothing Proj\left(\left\{A\right\}\times tagB\right)\right)$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		bj-projval	$$⊢\varnothing \in \mathrm{V}\to \left(\varnothing Proj\left(\left\{A\right\}\times tagB\right)\right)=if\left(A=\varnothing ,B,\varnothing \right)$$
4	2 3	ax-mp	$$⊢\left(\varnothing Proj\left(\left\{A\right\}\times tagB\right)\right)=if\left(A=\varnothing ,B,\varnothing \right)$$
5	1 4	eqtri	$$⊢pr1\left(\left\{A\right\}\times tagB\right)=if\left(A=\varnothing ,B,\varnothing \right)$$