Metamath Proof Explorer


Theorem brssrid

Description: Any set is a subset of itself. (Contributed by Peter Mazsa, 1-Aug-2019)

Ref Expression
Assertion brssrid ( 𝐴𝑉𝐴 S 𝐴 )

Proof

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