Theorem elqsecl

Description: Membership in a quotient set by an equivalence class according to .~ . (Contributed by Alexander van der Vekens, 12-Apr-2018) (Revised by AV, 30-Apr-2021)

	Ref	Expression
Assertion	elqsecl	⊢ ( 𝐵 ∈ 𝑋 → ( 𝐵 ∈ ( 𝑊 / ∼ ) ↔ ∃ 𝑥 ∈ 𝑊 𝐵 = { 𝑦 ∣ 𝑥 ∼ 𝑦 } ) )

Proof

Step	Hyp	Ref	Expression
1		elqsg	⊢ ( 𝐵 ∈ 𝑋 → ( 𝐵 ∈ ( 𝑊 / ∼ ) ↔ ∃ 𝑥 ∈ 𝑊 𝐵 = [ 𝑥 ] ∼ ) )
2		vex	⊢ 𝑥 ∈ V
3		dfec2	⊢ ( 𝑥 ∈ V → [ 𝑥 ] ∼ = { 𝑦 ∣ 𝑥 ∼ 𝑦 } )
4	2 3	mp1i	⊢ ( 𝐵 ∈ 𝑋 → [ 𝑥 ] ∼ = { 𝑦 ∣ 𝑥 ∼ 𝑦 } )
5	4	eqeq2d	⊢ ( 𝐵 ∈ 𝑋 → ( 𝐵 = [ 𝑥 ] ∼ ↔ 𝐵 = { 𝑦 ∣ 𝑥 ∼ 𝑦 } ) )
6	5	rexbidv	⊢ ( 𝐵 ∈ 𝑋 → ( ∃ 𝑥 ∈ 𝑊 𝐵 = [ 𝑥 ] ∼ ↔ ∃ 𝑥 ∈ 𝑊 𝐵 = { 𝑦 ∣ 𝑥 ∼ 𝑦 } ) )
7	1 6	bitrd	⊢ ( 𝐵 ∈ 𝑋 → ( 𝐵 ∈ ( 𝑊 / ∼ ) ↔ ∃ 𝑥 ∈ 𝑊 𝐵 = { 𝑦 ∣ 𝑥 ∼ 𝑦 } ) )