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 e. C ) -> A ~~ F )

Proof

Step Hyp Ref Expression
1 fnex
 |-  ( ( F Fn A /\ A e. C ) -> F e. _V )
2 fnfun
 |-  ( F Fn A -> Fun F )
3 2 adantr
 |-  ( ( F Fn A /\ A e. C ) -> Fun F )
4 fundmeng
 |-  ( ( F e. _V /\ Fun F ) -> dom F ~~ F )
5 1 3 4 syl2anc
 |-  ( ( F Fn A /\ A e. 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 e. C ) -> ( dom F ~~ F <-> A ~~ F ) )
9 5 8 mpbid
 |-  ( ( F Fn A /\ A e. C ) -> A ~~ F )