Theorem fvtp1

Description: The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	fvtp1.1	$$⊢A\in \mathrm{V}$$
	fvtp1.4	$$⊢D\in \mathrm{V}$$
Assertion	fvtp1	$$⊢\left(A\ne B\wedge A\ne C\right)\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(A\right)=D$$

Proof

Step	Hyp	Ref	Expression
1		fvtp1.1	$$⊢A\in \mathrm{V}$$
2		fvtp1.4	$$⊢D\in \mathrm{V}$$
3		df-tp	$$⊢\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}=\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}$$
4	3	fveq1i	$$⊢\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(A\right)=\left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)\left(A\right)$$
5		necom	$$⊢A\ne C\leftrightarrow C\ne A$$
6		fvunsn	$$⊢C\ne A\to \left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)\left(A\right)=\left\{⟨A,D⟩,⟨B,E⟩\right\}\left(A\right)$$
7	5 6	sylbi	$$⊢A\ne C\to \left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)\left(A\right)=\left\{⟨A,D⟩,⟨B,E⟩\right\}\left(A\right)$$
8	1 2	fvpr1	$$⊢A\ne B\to \left\{⟨A,D⟩,⟨B,E⟩\right\}\left(A\right)=D$$
9	7 8	sylan9eqr	$$⊢\left(A\ne B\wedge A\ne C\right)\to \left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)\left(A\right)=D$$
10	4 9	eqtrid	$$⊢\left(A\ne B\wedge A\ne C\right)\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(A\right)=D$$