Metamath Proof Explorer

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

Proof

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