Description: Alternate definition of a one-to-one function. (Contributed by NM, 31-Dec-1996)
Ref | Expression | ||
---|---|---|---|
Assertion | dff12 | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f1 | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ) | |
2 | funcnv2 | ⊢ ( Fun ◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) | |
3 | 2 | anbi2i | ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) ) |
4 | 1 3 | bitri | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) ) |