Theorem vsnex 5400

Description: A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.)

Assertion

Ref	Expression
vsnex	⊢ {𝑥} ∈ V

Proof of Theorem vsnex

Step	Hyp	Ref	Expression
1		dfsn2 4597	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5399	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2856	1 ⊢ {𝑥} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  snexgALT  5406  rext  5423  sspwb  5424  moabex  5433  moabexOLD  5434  nnullss  5437  exss  5438  xpsspw  5790  funopg  6568  snnex  7758  soex  7919  opabex3d  7963  opabex3rd  7964  opabex3  7965  fo1st  8007  fo2nd  8008  mpoexxg  8075  cnvf1o  8109  sexp2  8145  sexp3  8152  naddcllem  8665  domunsn  9126  fodomr  9127  findcard2  9160  pwfilem  9288  marypha1lem  9404  brwdom2  9546  unxpwdom2  9561  elirrvOLDOLD  9572  epfrs  9711  dfac5lem2  10128  dfac5lem3  10129  dfac5lem4  10130  kmlem2  10155  isfin1-3  10389  hsmexlem4  10432  axcc2lem  10439  canthwe  10661  canthp1lem1  10662  uniwun  10750  rankcf  10787  hashmap  14501  hashbclem  14518  incexclem  15926  isfunc  17954  homaf  18120  symgvalstruct  19525  gsum2d2  20102  gsumcom2  20103  dprd2da  20172  mpfind  22332  pf1ind  22581  dishaus  23608  discmp  23624  dis2ndc  23687  dislly  23724  dis1stc  23726  unisngl  23754  1stckgen  23781  ptcmpfi  24040  isufil2  24135  cnextfval  24289  conway  28045  etaslts  28059  cofcutr  28190  istrkg2ld  28802  lfuhgr1v0e  29715  gsumpart  33504  gsumwrd2dccat  33519  esum2dlem  34603  esum2d  34604  esumiun  34605  carsgclctunlem1  34829  eulerpartlemgs2  34892  bnj1452  35562  fobigcup  36478  elsingles  36496  fnsingle  36497  fvsingle  36498  dfiota3  36501  funpartlem  36522  altxpsspw  36558  axtco  37091  ttcid  37112  ttcmin  37116  dfttc4lem2  37149  mh-inf3sn  37162  mh-infprim2bi  37167  bj-snsetex  37708  bj-elsngl  37713  f1omptsnlem  38091  mptsnunlem  38093  topdifinffinlem  38102  heiborlem3  38564  ispointN  40616  mzpincl  43580  mzpcompact2lem  43597  pwslnmlem1  43934  pwslnm  43936  permaxinf2lem  45836  mpct  46033  salexct3  47171  salgencntex  47172  salgensscntex  47173  sge0xp  47258  clnbgrval  48739  mpoexxg2  49269  tposideq  49815  discsntermlem  50497