This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	phphashrd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	phphashrd.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
Assertion	phphashrd	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		phphashrd.1	⊢ ( 𝜑 → 𝐵 ∈ Fin )
2		phphashrd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		phphashrd.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
4	3	eqcomd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐴 ) )
5	1 2 4	phphashd	⊢ ( 𝜑 → 𝐵 = 𝐴 )
6	5	eqcomd	⊢ ( 𝜑 → 𝐴 = 𝐵 )