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 2860	1 ⊢ {𝑥} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  {csn 4588  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  snexgALT  5406  rext  5423  sspwb  5424  moabex  5433  moabexOLD  5434  nnullss  5437  exss  5438  xpsspw  5796  funopg  6602  snnex  7804  soex  7967  opabex3d  8011  opabex3rd  8012  opabex3  8013  fo1st  8055  fo2nd  8056  mpoexxg  8123  cnvf1o  8159  sexp2  8200  sexp3  8207  naddcllem  8723  domunsn  9184  fodomr  9185  findcard2  9218  pwfilem  9347  marypha1lem  9462  brwdom2  9604  unxpwdom2  9619  elirrvOLDOLD  9630  epfrs  9769  dfac5lem2  10242  dfac5lem3  10243  dfac5lem4  10244  kmlem2  10269  isfin1-3  10503  hsmexlem4  10546  axcc2lem  10553  canthwe  10775  canthp1lem1  10776  uniwun  10864  rankcf  10901  hashmap  14621  hashbclem  14638  incexclem  16049  isfunc  18089  homaf  18255  symgvalstruct  19662  gsum2d2  20239  gsumcom2  20240  dprd2da  20309  mpfind  22479  pf1ind  22728  dishaus  23755  discmp  23771  dis2ndc  23834  dislly  23871  dis1stc  23873  unisngl  23901  1stckgen  23928  ptcmpfi  24187  isufil2  24282  cnextfval  24436  conway  28222  etaslts  28236  cofcutr  28367  istrkg2ld  28979  lfuhgr1v0e  29892  gsumpart  33723  gsumwrd2dccat  33738  esum2dlem  34835  esum2d  34836  esumiun  34837  carsgclctunlem1  35060  eulerpartlemgs2  35123  bnj1452  35793  elpssmo  36673  fobigcup  36877  elsingles  36895  fnsingle  36896  fvsingle  36897  dfiota3  36900  funpartlem  36921  altxpsspw  36957  axtco  37474  ttcid  37495  ttcmin  37499  dfttc4lem2  37532  mh-inf3sn  37545  mh-infprim2bi  37550  bj-snsetex  38091  bj-elsngl  38096  f1omptsnlem  38527  mptsnunlem  38529  topdifinffinlem  38538  negprop  38911  heiborlem3  39013  ispointN  41065  mzpincl  44011  mzpcompact2lem  44028  pwslnmlem1  44360  pwslnm  44362  permaxinf2lem  46266  mpct  46488  salexct3  47625  salgencntex  47626  salgensscntex  47627  sge0xp  47712  clnbgrval  49193  mpoexxg2  49781  tposideq  50332  discsntermlem  51039