Theorem phphashd

Description: Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	phphashd.1	|- ( ph -> A e. Fin )
	phphashd.2	|- ( ph -> B C_ A )
	phphashd.3	|- ( ph -> ( # ` A ) = ( # ` B ) )
Assertion	phphashd	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		phphashd.1	|- ( ph -> A e. Fin )
2		phphashd.2	|- ( ph -> B C_ A )
3		phphashd.3	|- ( ph -> ( # ` A ) = ( # ` B ) )
4	1 2	ssfid	|- ( ph -> B e. Fin )
5		hashen	|- ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
6	1 4 5	syl2anc	|- ( ph -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
7	3 6	mpbid	|- ( ph -> A ~~ B )
8	1 2 7	phpeqd	|- ( ph -> A = B )