Metamath Proof Explorer


Theorem brcnvssrid

Description: Any set is a converse subset of itself. (Contributed by Peter Mazsa, 9-Jun-2021)

Ref Expression
Assertion brcnvssrid ( 𝐴𝑉𝐴 S 𝐴 )

Proof

Step Hyp Ref Expression
1 ssid 𝐴𝐴
2 brcnvssr ( 𝐴𝑉 → ( 𝐴 S 𝐴𝐴𝐴 ) )
3 1 2 mpbiri ( 𝐴𝑉𝐴 S 𝐴 )