Metamath Proof Explorer

Theorem relbrcnvg

Description: When R is a relation, the sethood assumptions on brcnv can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion relbrcnvg ⊢ Rel ⁡ R → A R -1 B ↔ B R A

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ R -1
2 1 brrelex12i ⊢ A R -1 B → A ∈ V ∧ B ∈ V
3 2 a1i ⊢ Rel ⁡ R → A R -1 B → A ∈ V ∧ B ∈ V
4 brrelex12 ⊢ Rel ⁡ R ∧ B R A → B ∈ V ∧ A ∈ V
5 4 ancomd ⊢ Rel ⁡ R ∧ B R A → A ∈ V ∧ B ∈ V
6 5 ex ⊢ Rel ⁡ R → B R A → A ∈ V ∧ B ∈ V
7 brcnvg ⊢ A ∈ V ∧ B ∈ V → A R -1 B ↔ B R A
8 7 a1i ⊢ Rel ⁡ R → A ∈ V ∧ B ∈ V → A R -1 B ↔ B R A
9 3 6 8 pm5.21ndd ⊢ Rel ⁡ R → A R -1 B ↔ B R A