Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Subset relations
brcnvssrid
Next ⟩
br1cossxrncnvssrres
Metamath Proof Explorer
Ascii
Unicode
Theorem
brcnvssrid
Description:
Any set is a converse subset of itself.
(Contributed by
Peter Mazsa
, 9-Jun-2021)
Ref
Expression
Assertion
brcnvssrid
⊢
A
∈
V
→
A
S
-1
A
Proof
Step
Hyp
Ref
Expression
1
ssid
⊢
A
⊆
A
2
brcnvssr
⊢
A
∈
V
→
A
S
-1
A
↔
A
⊆
A
3
1
2
mpbiri
⊢
A
∈
V
→
A
S
-1
A