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 ( 𝐴𝑉 → ( 𝐴 S 𝐵𝐵𝐴 ) )

Proof

Step Hyp Ref Expression
1 relssr Rel S
2 1 relbrcnv ( 𝐴 S 𝐵𝐵 S 𝐴 )
3 brssr ( 𝐴𝑉 → ( 𝐵 S 𝐴𝐵𝐴 ) )
4 2 3 syl5bb ( 𝐴𝑉 → ( 𝐴 S 𝐵𝐵𝐴 ) )