f1ocpbl

Description: An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015)

		Ref	Expression
	Hypothesis	f1ocpbl.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} X$
	Assertion	f1ocpbl	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((F (A) = F (C) \land F (B) = F (D)) \to F (A \underset{˙}{+} B) = F (C \underset{˙}{+} D))$

Step	Hyp	Ref	Expression
1		f1ocpbl.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} X$
2	1	f1ocpbllem	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((F (A) = F (C) \land F (B) = F (D)) \leftrightarrow (A = C \land B = D))$
3		oveq12	$⊢ (A = C \land B = D) \to A \underset{˙}{+} B = C \underset{˙}{+} D$
4	3	fveq2d	$⊢ (A = C \land B = D) \to F (A \underset{˙}{+} B) = F (C \underset{˙}{+} D)$
5	2 4	biimtrdi	$⊢ (φ \land (A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((F (A) = F (C) \land F (B) = F (D)) \to F (A \underset{˙}{+} B) = F (C \underset{˙}{+} D))$

Metamath Proof Explorer