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 e. V -> ( A `' _S B <-> B C_ A ) )

Proof

Step Hyp Ref Expression
1 relssr 
 |-  Rel _S
2 1 relbrcnv 
 |-  ( A `' _S B <-> B _S A )
3 brssr 
 |-  ( A e. V -> ( B _S A <-> B C_ A ) )
4 2 3 syl5bb 
 |-  ( A e. V -> ( A `' _S B <-> B C_ A ) )