fvtp1g

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

Step	Hyp	Ref	Expression
1		df-tp	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} = \{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}$
2	1	fveq1i	$⊢ \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (A) = (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A)$
3		necom	$⊢ A \neq C \leftrightarrow C \neq A$
4		fvunsn	$⊢ C \neq A \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = \{⟨A, D⟩, ⟨B, E⟩\} (A)$
5	3 4	sylbi	$⊢ A \neq C \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = \{⟨A, D⟩, ⟨B, E⟩\} (A)$
6	5	ad2antll	$⊢ ((A \in V \land D \in W) \land (A \neq B \land A \neq C)) \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = \{⟨A, D⟩, ⟨B, E⟩\} (A)$
7		fvpr1g	$⊢ (A \in V \land D \in W \land A \neq B) \to \{⟨A, D⟩, ⟨B, E⟩\} (A) = D$
8	7	3expa	$⊢ ((A \in V \land D \in W) \land A \neq B) \to \{⟨A, D⟩, ⟨B, E⟩\} (A) = D$
9	8	adantrr	$⊢ ((A \in V \land D \in W) \land (A \neq B \land A \neq C)) \to \{⟨A, D⟩, ⟨B, E⟩\} (A) = D$
10	6 9	eqtrd	$⊢ ((A \in V \land D \in W) \land (A \neq B \land A \neq C)) \to (\{⟨A, D⟩, ⟨B, E⟩\} \cup \{⟨C, F⟩\}) (A) = D$
11	2 10	syl5eq	$⊢ ((A \in V \land D \in W) \land (A \neq B \land A \neq C)) \to \{⟨A, D⟩, ⟨B, E⟩, ⟨C, F⟩\} (A) = D$

Metamath Proof Explorer