Metamath Proof Explorer

Theorem bj-snglsstag

Description: The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-snglsstag 
|- sngl A C_ tag A

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  sngl A C_ ( sngl A u. { (/) } )
2 df-bj-tag 
 |-  tag A = ( sngl A u. { (/) } )
3 1 2 sseqtrri 
 |-  sngl A C_ tag A