fvtp2

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

Step	Hyp	Ref	Expression
1		fvtp2.1	$⊢ B \in V$
2		fvtp2.4	$⊢ E \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⟩\} (B) = \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B)$
5		necom	$⊢ A \neq B \leftrightarrow B \neq A$
6	1 2	fvtp1	$⊢ (B \neq C \land B \neq A) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E$
7	6	ancoms	$⊢ (B \neq A \land B \neq C) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E$
8	5 7	sylanb	$⊢ (A \neq B \land B \neq C) \to \{⟨B, E⟩, ⟨C, F⟩, ⟨A, D⟩\} (B) = E$
9	4 8	eqtrid	$⊢ (A \neq B \land B \neq C) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (B) = E$

Metamath Proof Explorer