Theorem f1oeng

Description: The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998)

	Ref	Expression
Assertion	f1oeng	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fornex	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )
2		f1ofo	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
3	1 2	impel	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐵 ∈ V )
4		f1oen2g	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
5	4	3com23	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ≈ 𝐵 )
6	3 5	mpd3an3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )