# Metamath Proof Explorer

## Definition df-singleton

Description: Define the singleton function. See brsingle for its value. (Contributed by Scott Fenton, 4-Apr-2014)

Ref Expression
Assertion df-singleton ${⊢}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 csingle ${class}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$
1 cvv ${class}\mathrm{V}$
2 1 1 cxp ${class}\left(\mathrm{V}×\mathrm{V}\right)$
3 cep ${class}\mathrm{E}$
4 1 3 ctxp ${class}\left(\mathrm{V}\otimes \mathrm{E}\right)$
5 cid ${class}\mathrm{I}$
6 5 1 ctxp ${class}\left(\mathrm{I}\otimes \mathrm{V}\right)$
7 4 6 csymdif ${class}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$
8 7 crn ${class}\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$
9 2 8 cdif ${class}\left(\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)\right)$
10 0 9 wceq ${wff}\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}=\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\mathrm{I}\otimes \mathrm{V}\right)\right)$