Description: A function is equinumerous to its domain. Exercise 4 of Suppes p. 98. (Contributed by NM, 17-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | fundmeng | ⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → dom 𝐹 ≈ 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funeq | ⊢ ( 𝑥 = 𝐹 → ( Fun 𝑥 ↔ Fun 𝐹 ) ) | |
2 | dmeq | ⊢ ( 𝑥 = 𝐹 → dom 𝑥 = dom 𝐹 ) | |
3 | id | ⊢ ( 𝑥 = 𝐹 → 𝑥 = 𝐹 ) | |
4 | 2 3 | breq12d | ⊢ ( 𝑥 = 𝐹 → ( dom 𝑥 ≈ 𝑥 ↔ dom 𝐹 ≈ 𝐹 ) ) |
5 | 1 4 | imbi12d | ⊢ ( 𝑥 = 𝐹 → ( ( Fun 𝑥 → dom 𝑥 ≈ 𝑥 ) ↔ ( Fun 𝐹 → dom 𝐹 ≈ 𝐹 ) ) ) |
6 | vex | ⊢ 𝑥 ∈ V | |
7 | 6 | fundmen | ⊢ ( Fun 𝑥 → dom 𝑥 ≈ 𝑥 ) |
8 | 5 7 | vtoclg | ⊢ ( 𝐹 ∈ 𝑉 → ( Fun 𝐹 → dom 𝐹 ≈ 𝐹 ) ) |
9 | 8 | imp | ⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → dom 𝐹 ≈ 𝐹 ) |