Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Subset relations
issetssr
Next ⟩
brssrres
Metamath Proof Explorer
Ascii
Unicode
Theorem
issetssr
Description:
Two ways of expressing set existence.
(Contributed by
Peter Mazsa
, 1-Aug-2019)
Ref
Expression
Assertion
issetssr
⊢
A
∈
V
↔
A
S
A
Proof
Step
Hyp
Ref
Expression
1
brssrid
⊢
A
∈
V
→
A
S
A
2
relssr
⊢
Rel
⁡
S
3
2
brrelex1i
⊢
A
S
A
→
A
∈
V
4
1
3
impbii
⊢
A
∈
V
↔
A
S
A