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

Metamath Proof Explorer

Theorem dff14b

Description: A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018)

Ref Expression
Assertion dff14b ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A ∖ x F ⁡ x ≠ F ⁡ y

Proof

Step Hyp Ref Expression
1 dff14a ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A x ≠ y → F ⁡ x ≠ F ⁡ y
2 necom ⊢ x ≠ y ↔ y ≠ x
3 2 imbi1i ⊢ x ≠ y → F ⁡ x ≠ F ⁡ y ↔ y ≠ x → F ⁡ x ≠ F ⁡ y
4 3 ralbii ⊢ ∀ y ∈ A x ≠ y → F ⁡ x ≠ F ⁡ y ↔ ∀ y ∈ A y ≠ x → F ⁡ x ≠ F ⁡ y
5 raldifsnb ⊢ ∀ y ∈ A y ≠ x → F ⁡ x ≠ F ⁡ y ↔ ∀ y ∈ A ∖ x F ⁡ x ≠ F ⁡ y
6 4 5 bitri ⊢ ∀ y ∈ A x ≠ y → F ⁡ x ≠ F ⁡ y ↔ ∀ y ∈ A ∖ x F ⁡ x ≠ F ⁡ y
7 6 ralbii ⊢ ∀ x ∈ A ∀ y ∈ A x ≠ y → F ⁡ x ≠ F ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A ∖ x F ⁡ x ≠ F ⁡ y
8 7 anbi2i ⊢ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A x ≠ y → F ⁡ x ≠ F ⁡ y ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A ∖ x F ⁡ x ≠ F ⁡ y
9 1 8 bitri ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A ∖ x F ⁡ x ≠ F ⁡ y