Description: Closed form of elqs . (Contributed by Rodolfo Medina, 12-Oct-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | elqsg | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] 𝑅 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 | ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = [ 𝑥 ] 𝑅 ↔ 𝐵 = [ 𝑥 ] 𝑅 ) ) | |
2 | 1 | rexbidv | ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] 𝑅 ) ) |
3 | df-qs | ⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } | |
4 | 2 3 | elab2g | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 = [ 𝑥 ] 𝑅 ) ) |