Theorem bj-elsngl

Description: Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-elsngl	⊢ ( 𝐴 ∈ sngl 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝐴 ∈ sngl 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ sngl 𝐵 ) )
2		df-bj-sngl	⊢ sngl 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } }
3	2	abeq2i	⊢ ( 𝑦 ∈ sngl 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } )
4	3	anbi2i	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ sngl 𝐵 ) ↔ ( 𝑦 = 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } ) )
5	4	exbii	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ sngl 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } ) )
6		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) ↔ ( 𝑦 = 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } ) )
7	6	bicomi	⊢ ( ( 𝑦 = 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) )
8	7	exbii	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐵 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) )
9		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐵 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) )
10	9	bicomi	⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐵 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) )
11		eqcom	⊢ ( 𝐴 = { 𝑥 } ↔ { 𝑥 } = 𝐴 )
12		snex	⊢ { 𝑥 } ∈ V
13	12	eqvinc	⊢ ( { 𝑥 } = 𝐴 ↔ ∃ 𝑦 ( 𝑦 = { 𝑥 } ∧ 𝑦 = 𝐴 ) )
14		exancom	⊢ ( ∃ 𝑦 ( 𝑦 = { 𝑥 } ∧ 𝑦 = 𝐴 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) )
15	11 13 14	3bitri	⊢ ( 𝐴 = { 𝑥 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) )
16	15	bicomi	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) ↔ 𝐴 = { 𝑥 } )
17	16	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } )
18	8 10 17	3bitri	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 𝑦 = { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } )
19	1 5 18	3bitri	⊢ ( 𝐴 ∈ sngl 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝐴 = { 𝑥 } )