Metamath Proof Explorer

Theorem fvpr2gOLD

Description: Obsolete version of fvpr2g as of 26-Sep-2024. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	fvpr2gOLD	$⊢ (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		df-pr	$⊢ \{⟨B, D⟩, ⟨A, C⟩\} = \{⟨B, D⟩\} \cup \{⟨A, C⟩\}$
3	1 2	eqtri	$⊢ \{⟨A, C⟩, ⟨B, D⟩\} = \{⟨B, D⟩\} \cup \{⟨A, C⟩\}$
4	3	fveq1i	$⊢ \{⟨A, C⟩, ⟨B, D⟩\} (B) = (\{⟨B, D⟩\} \cup \{⟨A, C⟩\}) (B)$
5		fvunsn	$⊢ A \neq B \to (\{⟨B, D⟩\} \cup \{⟨A, C⟩\}) (B) = \{⟨B, D⟩\} (B)$
6	4 5	eqtrid	$⊢ A \neq B \to \{⟨A, C⟩, ⟨B, D⟩\} (B) = \{⟨B, D⟩\} (B)$
7	6	3ad2ant3	$⊢ (B \in V \land D \in W \land A \neq B) \to \{⟨A, C⟩, ⟨B, D⟩\} (B) = \{⟨B, D⟩\} (B)$
8		fvsng	$⊢ (B \in V \land D \in W) \to \{⟨B, D⟩\} (B) = D$
9	8	3adant3	$⊢ (B \in V \land D \in W \land A \neq B) \to \{⟨B, D⟩\} (B) = D$
10	7 9	eqtrd	$⊢ (B \in V \land D \in W \land A \neq B) \to \{⟨A, C⟩, ⟨B, D⟩\} (B) = D$