fvtp3g

Description: The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

		Ref	Expression
	Assertion	fvtp3g	$⊢ ((C \in V \land F \in W) \land (A \neq C \land B \neq C)) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (C) = F$

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

Metamath Proof Explorer