Theorem f1oen3g

Description: The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by NM, 13-Jan-2007) (Revised by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	f1oen3g	$$⊢\left(F\in V\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to A\approx B$$

Proof

Step	Hyp	Ref	Expression
1		f1oeq1	$$⊢f=F\to \left(f:A\underset{1-1\; onto}{⟶}B\leftrightarrow F:A\underset{1-1\; onto}{⟶}B\right)$$
2	1	spcegv	$$⊢F\in V\to \left(F:A\underset{1-1\; onto}{⟶}B\to \exists ff:A\underset{1-1\; onto}{⟶}B\right)$$
3	2	imp	$$⊢\left(F\in V\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to \exists ff:A\underset{1-1\; onto}{⟶}B$$
4		bren	$$⊢A\approx B\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}B$$
5	3 4	sylibr	$$⊢\left(F\in V\wedge F:A\underset{1-1\; onto}{⟶}B\right)\to A\approx B$$