Theorem hasheqf1od

Description: The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by AV, 4-May-2021)

	Ref	Expression
Hypotheses	hasheqf1od.a	|- ( ph -> A e. U )
	hasheqf1od.f	|- ( ph -> F : A -1-1-onto-> B )
Assertion	hasheqf1od	|- ( ph -> ( # ` A ) = ( # ` B ) )

Proof

Step	Hyp	Ref	Expression
1		hasheqf1od.a	|- ( ph -> A e. U )
2		hasheqf1od.f	|- ( ph -> F : A -1-1-onto-> B )
3		f1of	|- ( F : A -1-1-onto-> B -> F : A --> B )
4	2 3	syl	|- ( ph -> F : A --> B )
5	4 1	fexd	|- ( ph -> F e. _V )
6		f1oeq1	|- ( f = F -> ( f : A -1-1-onto-> B <-> F : A -1-1-onto-> B ) )
7	5 2 6	spcedv	|- ( ph -> E. f f : A -1-1-onto-> B )
8		hasheqf1oi	|- ( A e. U -> ( E. f f : A -1-1-onto-> B -> ( # ` A ) = ( # ` B ) ) )
9	1 7 8	sylc	|- ( ph -> ( # ` A ) = ( # ` B ) )