Metamath Proof Explorer

Theorem brcnvepres

Description: Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018)

Ref Expression
Assertion brcnvepres ⊢ B ∈ V ∧ C ∈ W → B E -1 ↾ A C ↔ B ∈ A ∧ C ∈ B

Proof

Step Hyp Ref Expression
1 brres ⊢ C ∈ W → B E -1 ↾ A C ↔ B ∈ A ∧ B E -1 C
2 brcnvep ⊢ B ∈ V → B E -1 C ↔ C ∈ B
3 2 anbi2d ⊢ B ∈ V → B ∈ A ∧ B E -1 C ↔ B ∈ A ∧ C ∈ B
4 1 3 sylan9bbr ⊢ B ∈ V ∧ C ∈ W → B E -1 ↾ A C ↔ B ∈ A ∧ C ∈ B