fvtp1

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

Step	Hyp	Ref	Expression
1		fvtp1.1	$⊢ A \in V$
2		fvtp1.4	$⊢ D \in V$
3		df-tp	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} = \{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}$
4	3	fveq1i	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (A) = (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A)$
5		necom	$⊢ A \neq C \leftrightarrow C \neq A$
6		fvunsn	$⊢ C \neq A \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = \{⟨A, D⟩, ⟨B, E⟩\} (A)$
7	5 6	sylbi	$⊢ A \neq C \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = \{⟨A, D⟩, ⟨B, E⟩\} (A)$
8	1 2	fvpr1	$⊢ A \neq B \to \{⟨A, D⟩, ⟨B, E⟩\} (A) = D$
9	7 8	sylan9eqr	$⊢ (A \neq B \land A \neq C) \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = D$
10	4 9	eqtrid	$⊢ (A \neq B \land A \neq C) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (A) = D$

Metamath Proof Explorer