Metamath Proof Explorer


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