fvtp2g

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	fvtp2g	$⊢ ((B \in V \land E \in W) \land (A \neq B \land B \neq C)) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (B) = E$

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⟩\} (B) = \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B)$
3		necom	$⊢ A \neq B \leftrightarrow B \neq A$
4		fvtp1g	$⊢ ((B \in V \land E \in W) \land (B \neq C \land B \neq A)) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E$
5	4	expcom	$⊢ (B \neq C \land B \neq A) \to ((B \in V \land E \in W) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E)$
6	5	ancoms	$⊢ (B \neq A \land B \neq C) \to ((B \in V \land E \in W) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E)$
7	3 6	sylanb	$⊢ (A \neq B \land B \neq C) \to ((B \in V \land E \in W) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E)$
8	7	impcom	$⊢ ((B \in V \land E \in W) \land (A \neq B \land B \neq C)) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E$
9	2 8	syl5eq	$⊢ ((B \in V \land E \in W) \land (A \neq B \land B \neq C)) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (B) = E$

Metamath Proof Explorer