Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-tagn0
Next ⟩
bj-tagss
Metamath Proof Explorer
Ascii
Structured
Theorem
bj-tagn0
Description:
The tagging of a class is nonempty.
(Contributed by
BJ
, 6-Apr-2019)
Ref
Expression
Assertion
bj-tagn0
⊢
tag
𝐴
≠ ∅
Proof
Step
Hyp
Ref
Expression
1
bj-0eltag
⊢
∅ ∈ tag
𝐴
2
1
ne0ii
⊢
tag
𝐴
≠ ∅