Metamath Proof Explorer


Theorem fndmeng

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

Ref Expression
Assertion fndmeng ( ( 𝐹 Fn 𝐴𝐴𝐶 ) → 𝐴𝐹 )

Proof

Step Hyp Ref Expression
1 fnex ( ( 𝐹 Fn 𝐴𝐴𝐶 ) → 𝐹 ∈ V )
2 fnfun ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3 2 adantr ( ( 𝐹 Fn 𝐴𝐴𝐶 ) → Fun 𝐹 )
4 fundmeng ( ( 𝐹 ∈ V ∧ Fun 𝐹 ) → dom 𝐹𝐹 )
5 1 3 4 syl2anc ( ( 𝐹 Fn 𝐴𝐴𝐶 ) → dom 𝐹𝐹 )
6 fndm ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7 6 breq1d ( 𝐹 Fn 𝐴 → ( dom 𝐹𝐹𝐴𝐹 ) )
8 7 adantr ( ( 𝐹 Fn 𝐴𝐴𝐶 ) → ( dom 𝐹𝐹𝐴𝐹 ) )
9 5 8 mpbid ( ( 𝐹 Fn 𝐴𝐴𝐶 ) → 𝐴𝐹 )