Metamath Proof Explorer

Theorem fndmeng

Description: A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion fndmeng ⊢ F Fn A ∧ A ∈ C → A ≈ F

Proof

Step Hyp Ref Expression
1 fnex ⊢ F Fn A ∧ A ∈ C → F ∈ V
2 fnfun ⊢ F Fn A → Fun ⁡ F
3 2 adantr ⊢ F Fn A ∧ A ∈ C → Fun ⁡ F
4 fundmeng ⊢ F ∈ V ∧ Fun ⁡ F → dom ⁡ F ≈ F
5 1 3 4 syl2anc ⊢ F Fn A ∧ A ∈ C → dom ⁡ F ≈ F
6 fndm ⊢ F Fn A → dom ⁡ F = A
7 6 breq1d ⊢ F Fn A → dom ⁡ F ≈ F ↔ A ≈ F
8 7 adantr ⊢ F Fn A ∧ A ∈ C → dom ⁡ F ≈ F ↔ A ≈ F
9 5 8 mpbid ⊢ F Fn A ∧ A ∈ C → A ≈ F