Metamath Proof Explorer


Theorem hashsn01

Description: The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021)

Ref Expression
Assertion hashsn01 A = 0 A = 1

Proof

Step Hyp Ref Expression
1 hashsng A V A = 1
2 1 olcd A V A = 0 A = 1
3 snprc ¬ A V A =
4 3 biimpi ¬ A V A =
5 4 fveq2d ¬ A V A =
6 hash0 = 0
7 5 6 eqtrdi ¬ A V A = 0
8 7 orcd ¬ A V A = 0 A = 1
9 2 8 pm2.61i A = 0 A = 1