Metamath Proof Explorer

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 ⊢ B ∈ A → B R ↾ A = B R

Proof

Step Hyp Ref Expression
1 elecres ⊢ y ∈ V → y ∈ B R ↾ A ↔ B ∈ A ∧ B R y
2 1 elv ⊢ y ∈ B R ↾ A ↔ B ∈ A ∧ B R y
3 2 baib ⊢ B ∈ A → y ∈ B R ↾ A ↔ B R y
4 3 eqabdv ⊢ B ∈ A → B R ↾ A = y | B R y
5 dfec2 ⊢ B ∈ A → B R = y | B R y
6 4 5 eqtr4d ⊢ B ∈ A → B R ↾ A = B R