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

Metamath Proof Explorer

Theorem brcnvssr

Description: The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019)

Ref Expression
Assertion brcnvssr ⊢ A ∈ V → A S -1 B ↔ B ⊆ A

Proof

Step Hyp Ref Expression
1 relssr ⊢ Rel ⁡ S
2 1 relbrcnv ⊢ A S -1 B ↔ B S A
3 brssr ⊢ A ∈ V → B S A ↔ B ⊆ A
4 2 3 bitrid ⊢ A ∈ V → A S -1 B ↔ B ⊆ A