Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-snglinv
Next ⟩
bj-snglex
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-snglinv
Description:
Inverse of singletonization.
(Contributed by
BJ
, 6-Oct-2018)
Ref
Expression
Assertion
bj-snglinv
⊢
A
=
x
|
x
∈
sngl
A
Proof
Step
Hyp
Ref
Expression
1
bj-snglc
⊢
x
∈
A
↔
x
∈
sngl
A
2
1
abbi2i
⊢
A
=
x
|
x
∈
sngl
A