Metamath Proof Explorer

Theorem ec1cnvres

Description: Converse restricted coset of B . (Contributed by Peter Mazsa, 22-Mar-2019) (Revised by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion ec1cnvres ⊢ B ∈ V → B R ↾ A -1 = x ∈ A | x R B

Proof

Step Hyp Ref Expression
1 elec1cnvres ⊢ B ∈ V → x ∈ B R ↾ A -1 ↔ x ∈ A ∧ x R B
2 1 eqabdv ⊢ B ∈ V → B R ↾ A -1 = x | x ∈ A ∧ x R B
3 df-rab ⊢ x ∈ A | x R B = x | x ∈ A ∧ x R B
4 2 3 eqtr4di ⊢ B ∈ V → B R ↾ A -1 = x ∈ A | x R B