Theorem fvpr2g

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

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

Proof

Step	Hyp	Ref	Expression
1		prcom	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}=\left\{⟨B,D⟩,⟨A,C⟩\right\}$$
2	1	fveq1i	$$⊢\left\{⟨A,C⟩,⟨B,D⟩\right\}\left(B\right)=\left\{⟨B,D⟩,⟨A,C⟩\right\}\left(B\right)$$
3		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
4		fvpr1g	$$⊢\left(B\in V\wedge D\in W\wedge B\ne A\right)\to \left\{⟨B,D⟩,⟨A,C⟩\right\}\left(B\right)=D$$
5	3 4	syl3an3b	$$⊢\left(B\in V\wedge D\in W\wedge A\ne B\right)\to \left\{⟨B,D⟩,⟨A,C⟩\right\}\left(B\right)=D$$
6	2 5	syl5eq	$$⊢\left(B\in V\wedge D\in W\wedge A\ne B\right)\to \left\{⟨A,C⟩,⟨B,D⟩\right\}\left(B\right)=D$$