Metamath Proof Explorer


Theorem snelsingles

Description: A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Hypothesis snelsingles.1 A V
Assertion snelsingles A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌

Proof

Step Hyp Ref Expression
1 snelsingles.1 A V
2 isset A V x x = A
3 eqcom x = A A = x
4 3 exbii x x = A x A = x
5 2 4 bitri A V x A = x
6 1 5 mpbi x A = x
7 sneq A = x A = x
8 6 7 eximii x A = x
9 elsingles A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 x A = x
10 8 9 mpbir A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌