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

Metamath Proof Explorer

Theorem hashdifsn

Description: The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018)

Ref Expression
Assertion hashdifsn ⊢ A ∈ Fin ∧ B ∈ A → A ∖ B = A − 1

Proof

Step Hyp Ref Expression
1 snssi ⊢ B ∈ A → B ⊆ A
2 hashssdif ⊢ A ∈ Fin ∧ B ⊆ A → A ∖ B = A − B
3 1 2 sylan2 ⊢ A ∈ Fin ∧ B ∈ A → A ∖ B = A − B
4 hashsng ⊢ B ∈ A → B = 1
5 4 adantl ⊢ A ∈ Fin ∧ B ∈ A → B = 1
6 5 oveq2d ⊢ A ∈ Fin ∧ B ∈ A → A − B = A − 1
7 3 6 eqtrd ⊢ A ∈ Fin ∧ B ∈ A → A ∖ B = A − 1