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	$$⊢\phi \to A\in \mathrm{Fin}$$
	phphashd.2	$$⊢\phi \to B\subseteq A$$
	phphashd.3	$$⊢\phi \to \left|A\right|=\left|B\right|$$
Assertion	phphashd	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		phphashd.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		phphashd.2	$$⊢\phi \to B\subseteq A$$
3		phphashd.3	$$⊢\phi \to \left|A\right|=\left|B\right|$$
4	1 2	ssfid	$$⊢\phi \to B\in \mathrm{Fin}$$
5		hashen	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|B\right|\leftrightarrow A\approx B\right)$$
6	1 4 5	syl2anc	$$⊢\phi \to \left(\left|A\right|=\left|B\right|\leftrightarrow A\approx B\right)$$
7	3 6	mpbid	$$⊢\phi \to A\approx B$$
8	1 2 7	phpeqd	$$⊢\phi \to A=B$$