Theorem fvtp2

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

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

Proof

Step	Hyp	Ref	Expression
1		fvtp2.1	$$⊢B\in \mathrm{V}$$
2		fvtp2.4	$$⊢E\in \mathrm{V}$$
3		tprot	$$⊢\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}=\left\{⟨B,E⟩,⟨C,F⟩,⟨A,D⟩\right\}$$
4	3	fveq1i	$$⊢\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(B\right)=\left\{⟨B,E⟩,⟨C,F⟩,⟨A,D⟩\right\}\left(B\right)$$
5		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
6	1 2	fvtp1	$$⊢\left(B\ne C\wedge B\ne A\right)\to \left\{⟨B,E⟩,⟨C,F⟩,⟨A,D⟩\right\}\left(B\right)=E$$
7	6	ancoms	$$⊢\left(B\ne A\wedge B\ne C\right)\to \left\{⟨B,E⟩,⟨C,F⟩,⟨A,D⟩\right\}\left(B\right)=E$$
8	5 7	sylanb	$$⊢\left(A\ne B\wedge B\ne C\right)\to \left\{⟨B,E⟩,⟨C,F⟩,⟨A,D⟩\right\}\left(B\right)=E$$
9	4 8	syl5eq	$$⊢\left(A\ne B\wedge B\ne C\right)\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(B\right)=E$$