Theorem fvpr1g

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

	Ref	Expression
Assertion	fvpr1g	$$⊢\left(A\in V\wedge C\in W\wedge A\ne B\right)\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}$$
2	1	fveq1i	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=\left(\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}\right)\left(A\right)$$
3		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
4		fvunsn	$$⊢B\ne A\to \left(\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}\right)\left(A\right)=\left\{⟨A,C⟩\right\}\left(A\right)$$
5	3 4	sylbi	$$⊢A\ne B\to \left(\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}\right)\left(A\right)=\left\{⟨A,C⟩\right\}\left(A\right)$$
6	2 5	syl5eq	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=\left\{⟨A,C⟩\right\}\left(A\right)$$
7	6	3ad2ant3	$$⊢\left(A\in V\wedge C\in W\wedge A\ne B\right)\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=\left\{⟨A,C⟩\right\}\left(A\right)$$
8		fvsng	$$⊢\left(A\in V\wedge C\in W\right)\to \left\{⟨A,C⟩\right\}\left(A\right)=C$$
9	8	3adant3	$$⊢\left(A\in V\wedge C\in W\wedge A\ne B\right)\to \left\{⟨A,C⟩\right\}\left(A\right)=C$$
10	7 9	eqtrd	$$⊢\left(A\in V\wedge C\in W\wedge A\ne B\right)\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=C$$