Theorem elecreseq

Description: The restricted coset of B when B is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018)

	Ref	Expression
Assertion	elecreseq	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = [ 𝐵 ] 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		elecres	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) ) )
2	1	elv	⊢ ( 𝑦 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 𝑅 𝑦 ) )
3	2	baib	⊢ ( 𝐵 ∈ 𝐴 → ( 𝑦 ∈ [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ↔ 𝐵 𝑅 𝑦 ) )
4	3	eqabdv	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = { 𝑦 ∣ 𝐵 𝑅 𝑦 } )
5		dfec2	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 = { 𝑦 ∣ 𝐵 𝑅 𝑦 } )
6	4 5	eqtr4d	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = [ 𝐵 ] 𝑅 )