Metamath Proof Explorer


Theorem ecres2

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 ( 𝐵𝐴 → [ 𝐵 ] ( 𝑅𝐴 ) = [ 𝐵 ] 𝑅 )

Proof

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