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 𝐴 ∧ 𝐴 ∈ 𝐶 ) → 𝐴 ≈ 𝐹 )