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	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1oeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
2	1	spcegv	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
3	2	imp	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
4		bren	⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
5	3 4	sylibr	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )