Metamath Proof Explorer

Theorem bj-0eltag

Description: The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-0eltag 
|- (/) e. tag A

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 snid 
 |-  (/) e. { (/) }
3 2 olci 
 |-  ( (/) e. sngl A \/ (/) e. { (/) } )
4 elun 
 |-  ( (/) e. ( sngl A u. { (/) } ) <-> ( (/) e. sngl A \/ (/) e. { (/) } ) )
5 3 4 mpbir 
 |-  (/) e. ( sngl A u. { (/) } )
6 df-bj-tag 
 |-  tag A = ( sngl A u. { (/) } )
7 5 6 eleqtrri 
 |-  (/) e. tag A