Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Subset relations
brssrid
Next ⟩
issetssr
Metamath Proof Explorer
Ascii
Unicode
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