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

Metamath Proof Explorer

Theorem hashelne0d

Description: A set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses hashelne0d.1 ⊢ φ → B ∈ A
hashelne0d.2 ⊢ φ → A ∈ V
Assertion hashelne0d ⊢ φ → ¬ A = 0

Proof

Step Hyp Ref Expression
1 hashelne0d.1 ⊢ φ → B ∈ A
2 hashelne0d.2 ⊢ φ → A ∈ V
3 1 ne0d ⊢ φ → A ≠ ∅
4 3 neneqd ⊢ φ → ¬ A = ∅
5 hasheq0 ⊢ A ∈ V → A = 0 ↔ A = ∅
6 2 5 syl ⊢ φ → A = 0 ↔ A = ∅
7 4 6 mtbird ⊢ φ → ¬ A = 0