This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem br1cnvres

Description: Binary relation on the converse of a restriction. (Contributed by Peter Mazsa, 27-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 df-res ⊢ R ↾ A = R ∩ A × V
2 1 cnveqi ⊢ R ↾ A -1 = R ∩ A × V -1
3 2 breqi ⊢ B R ↾ A -1 C ↔ B R ∩ A × V -1 C
4 elex ⊢ B ∈ V → B ∈ V
5 br1cnvinxp ⊢ B R ∩ A × V -1 C ↔ B ∈ V ∧ C ∈ A ∧ C R B
6 anass ⊢ B ∈ V ∧ C ∈ A ∧ C R B ↔ B ∈ V ∧ C ∈ A ∧ C R B
7 5 6 bitri ⊢ B R ∩ A × V -1 C ↔ B ∈ V ∧ C ∈ A ∧ C R B
8 7 baib ⊢ B ∈ V → B R ∩ A × V -1 C ↔ C ∈ A ∧ C R B
9 4 8 syl ⊢ B ∈ V → B R ∩ A × V -1 C ↔ C ∈ A ∧ C R B
10 3 9 bitrid ⊢ B ∈ V → B R ↾ A -1 C ↔ C ∈ A ∧ C R B