Theorem bj-sngltag

Description: The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sngltag	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ sngl 𝐵 ↔ { 𝐴 } ∈ tag 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-sngltagi	⊢ ( { 𝐴 } ∈ sngl 𝐵 → { 𝐴 } ∈ tag 𝐵 )
2		df-bj-tag	⊢ tag 𝐵 = ( sngl 𝐵 ∪ { ∅ } )
3	2	eleq2i	⊢ ( { 𝐴 } ∈ tag 𝐵 ↔ { 𝐴 } ∈ ( sngl 𝐵 ∪ { ∅ } ) )
4		elun	⊢ ( { 𝐴 } ∈ ( sngl 𝐵 ∪ { ∅ } ) ↔ ( { 𝐴 } ∈ sngl 𝐵 ∨ { 𝐴 } ∈ { ∅ } ) )
5		idd	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ sngl 𝐵 → { 𝐴 } ∈ sngl 𝐵 ) )
6		elsni	⊢ ( { 𝐴 } ∈ { ∅ } → { 𝐴 } = ∅ )
7		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
8		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
9	8	pm2.24d	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ V → { 𝐴 } ∈ sngl 𝐵 ) )
10	7 9	syl5bir	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = ∅ → { 𝐴 } ∈ sngl 𝐵 ) )
11	6 10	syl5	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ { ∅ } → { 𝐴 } ∈ sngl 𝐵 ) )
12	5 11	jaod	⊢ ( 𝐴 ∈ 𝑉 → ( ( { 𝐴 } ∈ sngl 𝐵 ∨ { 𝐴 } ∈ { ∅ } ) → { 𝐴 } ∈ sngl 𝐵 ) )
13	4 12	syl5bi	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ ( sngl 𝐵 ∪ { ∅ } ) → { 𝐴 } ∈ sngl 𝐵 ) )
14	3 13	syl5bi	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ tag 𝐵 → { 𝐴 } ∈ sngl 𝐵 ) )
15	1 14	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ sngl 𝐵 ↔ { 𝐴 } ∈ tag 𝐵 ) )