Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-snglsstag
Next ⟩
bj-sngltagi
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-snglsstag
Description:
The singletonization is included in the tagging.
(Contributed by
BJ
, 6-Oct-2018)
Ref
Expression
Assertion
bj-snglsstag
⊢
sngl
A
⊆
tag
A
Proof
Step
Hyp
Ref
Expression
1
ssun1
⊢
sngl
A
⊆
sngl
A
∪
∅
2
df-bj-tag
⊢
tag
A
=
sngl
A
∪
∅
3
1
2
sseqtrri
⊢
sngl
A
⊆
tag
A