Metamath Proof Explorer


Theorem brssrid

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

Ref Expression
Assertion brssrid A V A S A

Proof

Step Hyp Ref Expression
1 ssid A A
2 brssr A V A S A A A
3 1 2 mpbiri A V A S A