Theorem bj-snglc

Description: Characterization of the elements of A in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-snglc	⊢ ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ∈ sngl 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 { 𝐴 } = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ { 𝐴 } = { 𝑥 } ) )
2		bj-elsngl	⊢ ( { 𝐴 } ∈ sngl 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 { 𝐴 } = { 𝑥 } )
3		elisset	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 = 𝐴 )
4	3	pm4.71i	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∃ 𝑥 𝑥 = 𝐴 ) )
5		19.42v	⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∃ 𝑥 𝑥 = 𝐴 ) )
6		eleq1	⊢ ( 𝐴 = 𝑥 → ( 𝐴 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
7	6	eqcoms	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
8	7	pm5.32ri	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) )
9	8	exbii	⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) )
10	4 5 9	3bitr2i	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) )
11		sneqbg	⊢ ( 𝑥 ∈ V → ( { 𝑥 } = { 𝐴 } ↔ 𝑥 = 𝐴 ) )
12	11	elv	⊢ ( { 𝑥 } = { 𝐴 } ↔ 𝑥 = 𝐴 )
13		eqcom	⊢ ( { 𝑥 } = { 𝐴 } ↔ { 𝐴 } = { 𝑥 } )
14	12 13	bitr3i	⊢ ( 𝑥 = 𝐴 ↔ { 𝐴 } = { 𝑥 } )
15	14	anbi2i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ { 𝐴 } = { 𝑥 } ) )
16	15	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ { 𝐴 } = { 𝑥 } ) )
17	10 16	bitri	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ { 𝐴 } = { 𝑥 } ) )
18	1 2 17	3bitr4ri	⊢ ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ∈ sngl 𝐵 )