Metamath Proof Explorer

Theorem bj-tagex

Description: A class is a set if and only if its tagging is a set. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-tagex ⊢ A ∈ V ↔ tag A ∈ V

Proof

Step Hyp Ref Expression
1 bj-snglex ⊢ A ∈ V ↔ sngl A ∈ V
2 p0ex ⊢ ∅ ∈ V
3 2 biantru ⊢ sngl A ∈ V ↔ sngl A ∈ V ∧ ∅ ∈ V
4 1 3 bitri ⊢ A ∈ V ↔ sngl A ∈ V ∧ ∅ ∈ V
5 unexb ⊢ sngl A ∈ V ∧ ∅ ∈ V ↔ sngl A ∪ ∅ ∈ V
6 df-bj-tag ⊢ tag A = sngl A ∪ ∅
7 6 eqcomi ⊢ sngl A ∪ ∅ = tag A
8 7 eleq1i ⊢ sngl A ∪ ∅ ∈ V ↔ tag A ∈ V
9 4 5 8 3bitri ⊢ A ∈ V ↔ tag A ∈ V