fvtp3

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

Step	Hyp	Ref	Expression
1		fvtp3.1	$⊢ C \in V$
2		fvtp3.4	$⊢ F \in V$
3		tprot	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} = \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\}$
4	3	fveq1i	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (C) = \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (C)$
5		necom	$⊢ A \neq C \leftrightarrow C \neq A$
6	1 2	fvtp2	$⊢ (B \neq C \land C \neq A) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (C) = F$
7	5 6	sylan2b	$⊢ (B \neq C \land A \neq C) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (C) = F$
8	7	ancoms	$⊢ (A \neq C \land B \neq C) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (C) = F$
9	4 8	eqtrid	$⊢ (A \neq C \land B \neq C) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (C) = F$

Metamath Proof Explorer