Theorem elqsg

Description: Closed form of elqs . (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Assertion	elqsg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝐵 = [ 𝑥 ] 𝑅 ) )
2	1	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] 𝑅 ) )
3		df-qs	⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
4	2 3	elab2g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] 𝑅 ) )