Metamath Proof Explorer

Theorem elec1cnvres

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

Ref Expression
Assertion elec1cnvres ⊢ B ∈ V → C ∈ B R ↾ A -1 ↔ C ∈ A ∧ C R B

Proof

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