Metamath Proof Explorer

Theorem hashrabsn01

Description: The size of a restricted class abstraction restricted to a singleton is either 0 or 1. (Contributed by Alexander van der Vekens, 3-Sep-2018)

Ref Expression
Assertion hashrabsn01 ⊢x∈A|φ=N→N=0∨N=1

Proof

Step Hyp Ref Expression
1 eqid ⊢x∈A|φ=x∈A|φ
2 rabrsn ⊢x∈A|φ=x∈A|φ→x∈A|φ=∅∨x∈A|φ=A
3 fveqeq2 ⊢x∈A|φ=∅→x∈A|φ=N↔∅=N
4 eqcom ⊢∅=N↔N=∅
5 4 biimpi ⊢∅=N→N=∅
6 hash0 ⊢∅=0
7 5 6 eqtrdi ⊢∅=N→N=0
8 7 orcd ⊢∅=N→N=0∨N=1
9 3 8 syl6bi ⊢x∈A|φ=∅→x∈A|φ=N→N=0∨N=1
10 fveqeq2 ⊢x∈A|φ=A→x∈A|φ=N↔A=N
11 eqcom ⊢A=N↔N=A
12 11 biimpi ⊢A=N→N=A
13 hashsng ⊢A∈V→A=1
14 12 13 sylan9eqr ⊢A∈V∧A=N→N=1
15 14 olcd ⊢A∈V∧A=N→N=0∨N=1
16 15 ex ⊢A∈V→A=N→N=0∨N=1
17 snprc ⊢¬A∈V↔A=∅
18 fveqeq2 ⊢A=∅→A=N↔∅=N
19 18 8 syl6bi ⊢A=∅→A=N→N=0∨N=1
20 17 19 sylbi ⊢¬A∈V→A=N→N=0∨N=1
21 16 20 pm2.61i ⊢A=N→N=0∨N=1
22 10 21 syl6bi ⊢x∈A|φ=A→x∈A|φ=N→N=0∨N=1
23 9 22 jaoi ⊢x∈A|φ=∅∨x∈A|φ=A→x∈A|φ=N→N=0∨N=1
24 1 2 23 mp2b ⊢x∈A|φ=N→N=0∨N=1