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 syl5bb A V A S -1 B B A