Metamath Proof Explorer

Theorem f1olecpbl

Description: An injection is compatible with any relations 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	f1olecpbl	$⊢ (φ \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 (A N B \leftrightarrow C N 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		breq12	$⊢ (A = C \land B = D) \to (A N B \leftrightarrow C N D)$
4	2 3	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 (A N B \leftrightarrow C N D))$