Theorem fvpr1

Description: The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010)

	Ref	Expression
Hypotheses	fvpr1.1	$$⊢A\in \mathrm{V}$$
	fvpr1.2	$$⊢C\in \mathrm{V}$$
Assertion	fvpr1	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		fvpr1.1	$$⊢A\in \mathrm{V}$$
2		fvpr1.2	$$⊢C\in \mathrm{V}$$
3		df-pr	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}$$
4	3	fveq1i	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=\left(\left\{⟨A,C⟩\right\}\cup \left\{⟨B,D⟩\right\}\right)\left(A\right)$$
5		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
6		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)$$
7	5 6	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)$$
8	4 7	syl5eq	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=\left\{⟨A,C⟩\right\}\left(A\right)$$
9	1 2	fvsn	$$⊢\left\{⟨A,C⟩\right\}\left(A\right)=C$$
10	8 9	eqtrdi	$$⊢A\ne B\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(A\right)=C$$