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	$$⊢\left(A\in C\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to A\approx B$$

Proof

Step	Hyp	Ref	Expression
1		focdmex	$$⊢A\in C\to \left(F:A\underset{onto}{⟶}B\to B\in \mathrm{V}\right)$$
2		f1ofo	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{onto}{⟶}B$$
3	1 2	impel	$$⊢\left(A\in C\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to B\in \mathrm{V}$$
4		f1oen2g	$$⊢\left(A\in C\wedge B\in \mathrm{V}\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to A\approx B$$
5	4	3com23	$$⊢\left(A\in C\wedge F:A\underset{1-1\; onto}{⟶}B\wedge B\in \mathrm{V}\right)\to A\approx B$$
6	3 5	mpd3an3	$$⊢\left(A\in C\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to A\approx B$$