Metamath Proof Explorer

Theorem rev0

Description: The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion rev0 ⊢ reverse ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 wrd0 ⊢ ∅ ∈ Word V
2 revlen ⊢ ∅ ∈ Word V → reverse ⁡ ∅ = ∅
3 1 2 ax-mp ⊢ reverse ⁡ ∅ = ∅
4 hash0 ⊢ ∅ = 0
5 3 4 eqtri ⊢ reverse ⁡ ∅ = 0
6 fvex ⊢ reverse ⁡ ∅ ∈ V
7 hasheq0 ⊢ reverse ⁡ ∅ ∈ V → reverse ⁡ ∅ = 0 ↔ reverse ⁡ ∅ = ∅
8 6 7 ax-mp ⊢ reverse ⁡ ∅ = 0 ↔ reverse ⁡ ∅ = ∅
9 5 8 mpbi ⊢ reverse ⁡ ∅ = ∅