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 )