This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → F : V ⟶ 1-1 onto X
Assertion f1olecpbl ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D → A N B ↔ C N D

Proof

Step Hyp Ref Expression
1 f1ocpbl.f ⊢ φ → F : V ⟶ 1-1 onto X
2 1 f1ocpbllem ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D ↔ A = C ∧ B = D
3 breq12 ⊢ A = C ∧ B = D → A N B ↔ C N D
4 2 3 biimtrdi ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D → A N B ↔ C N D