Theorem phphashrd

Description: Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	phphashrd.1	$$⊢\phi \to B\in \mathrm{Fin}$$
	phphashrd.2	$$⊢\phi \to A\subseteq B$$
	phphashrd.3	$$⊢\phi \to \left|A\right|=\left|B\right|$$
Assertion	phphashrd	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		phphashrd.1	$$⊢\phi \to B\in \mathrm{Fin}$$
2		phphashrd.2	$$⊢\phi \to A\subseteq B$$
3		phphashrd.3	$$⊢\phi \to \left|A\right|=\left|B\right|$$
4	3	eqcomd	$$⊢\phi \to \left|B\right|=\left|A\right|$$
5	1 2 4	phphashd	$$⊢\phi \to B=A$$
6	5	eqcomd	$$⊢\phi \to A=B$$