Metamath Proof Explorer

Theorem ecres

Description: Restricted coset of B . (Contributed by Peter Mazsa, 9-Dec-2018)

Ref Expression
Assertion ecres ⊢ B R ↾ A = x | B ∈ A ∧ B R x

Proof

Step Hyp Ref Expression
1 elecres ⊢ x ∈ V → x ∈ B R ↾ A ↔ B ∈ A ∧ B R x
2 1 elv ⊢ x ∈ B R ↾ A ↔ B ∈ A ∧ B R x
3 2 eqabi ⊢ B R ↾ A = x | B ∈ A ∧ B R x