Description: The restricted coset of B when B is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | ecres2 | ⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = [ 𝐵 ] 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elecres | ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) ) ) | |
2 | 1 | elv | ⊢ ( 𝑦 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) ) |
3 | 2 | baib | ⊢ ( 𝐵 ∈ 𝐴 → ( 𝑦 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ 𝐵 𝑅 𝑦 ) ) |
4 | 3 | abbi2dv | ⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = { 𝑦 ∣ 𝐵 𝑅 𝑦 } ) |
5 | dfec2 | ⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 = { 𝑦 ∣ 𝐵 𝑅 𝑦 } ) | |
6 | 4 5 | eqtr4d | ⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = [ 𝐵 ] 𝑅 ) |