Description: Restricted coset of B . (Contributed by Peter Mazsa, 9-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | ecres | ⊢ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = { 𝑥 ∣ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑥 ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elecres | ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑥 ) ) ) | |
2 | 1 | elv | ⊢ ( 𝑥 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑥 ) ) |
3 | 2 | abbi2i | ⊢ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = { 𝑥 ∣ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑥 ) } |