Metamath Proof Explorer

Theorem elecres

Description: Elementhood in the restricted coset of B . (Contributed by Peter Mazsa, 21-Sep-2018)

Ref Expression
Assertion elecres ⊢ C ∈ V → C ∈ B R ↾ A ↔ B ∈ A ∧ B R C

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ R ↾ A
2 relelec ⊢ Rel ⁡ R ↾ A → C ∈ B R ↾ A ↔ B R ↾ A C
3 1 2 ax-mp ⊢ C ∈ B R ↾ A ↔ B R ↾ A C
4 brres ⊢ C ∈ V → B R ↾ A C ↔ B ∈ A ∧ B R C
5 3 4 bitrid ⊢ C ∈ V → C ∈ B R ↾ A ↔ B ∈ A ∧ B R C