Metamath Proof Explorer


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 ( 𝐵𝑉 → ( 𝐵 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥𝐴 𝐵 = [ 𝑥 ] 𝑅 ) )