NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  snex Structured version   GIF version

Theorem snex 4111
Description: A singleton always exists. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
snex {A} V

Proof of Theorem snex
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 3744 . . . 4 (x = A → {x} = {A})
21eleq1d 2419 . . 3 (x = A → ({x} V ↔ {A} V))
3 ax-sn 4087 . . . 4 yz(z yz = x)
4 isset 2863 . . . . 5 ({x} V ↔ y y = {x})
5 axprimlem1 4088 . . . . . 6 (y = {x} ↔ z(z yz = x))
65exbii 1582 . . . . 5 (y y = {x} ↔ yz(z yz = x))
74, 6bitri 240 . . . 4 ({x} V ↔ yz(z yz = x))
83, 7mpbir 200 . . 3 {x} V
92, 8vtoclg 2914 . 2 (A V → {A} V)
10 snprc 3788 . . . 4 A V ↔ {A} = )
1110biimpi 186 . . 3 A V → {A} = )
12 0ex 4110 . . 3 V
1311, 12syl6eqel 2441 . 2 A V → {A} V)
149, 13pm2.61i 156 1 {A} V
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wb 176  wal 1540  wex 1541   = wceq 1642   wcel 1710  Vcvv 2859  c0 3550  {csn 3737
This theorem is referenced by:  prex  4112  snelpwg  4114  snelpwi  4116  sspwb  4118  pwadjoin  4119  elopk  4129  el1c  4139  elpw1  4144  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  eqpw1  4162  pw111  4170  eluni1g  4172  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  elp6  4263  opksnelsik  4265  elssetkg  4269  opkelimagekg  4271  ins2kss  4279  ins3kss  4280  dfuni12  4291  sikexlem  4295  sikexg  4296  dfimak2  4298  insklem  4304  ins2kexg  4305  ins3kexg  4306  dfuni3  4315  dfint3  4318  setswith  4321  setswithex  4322  ndisjrelk  4323  unipw1  4325  dfpw2  4327  dfaddc2  4381  0cex  4392  dfnnc2  4395  nnc0suc  4411  elsuc  4412  nnsucelrlem1  4423  nnsucelr  4427  nndisjeq  4428  preaddccan1lem1  4453  ltfinex  4464  ltfintrilem1  4465  ssfin  4470  ncfinsn  4476  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinraise  4481  ncfinlowerlem1  4482  ncfinlower  4483  eqtfinrelk  4486  tfinrelkex  4487  tfinsuc  4498  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  nnadjoinlem1  4519  nnadjoin  4520  nnadjoinpw  4521  nnpweqlem1  4522  srelk  4524  sfindbl  4530  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspnn  4541  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  nulnnn  4556  dfop2lem1  4573  opexg  4587  proj2exg  4592  proj2op  4599  setconslem1  4723  setconslem2  4724  setconslem3  4725  setconslem4  4726  setconslem5  4727  setconslem6  4728  setconslem7  4729  df1st2  4730  1stex  4731  dfswap2  4733  swapex  4734  brssetsn  4751  brsi  4753  elimapw1  4958  elimapw12  4959  elimapw13  4960  elimapw11c  4962  elxp4  5141  dmsi  5561  brsnsi  5803  brimage  5822  addcfnex  5852  funsex  5856  crossex  5876  pw1fnex  5878  pw1fnf1o  5881  fullfunexg  5885  clos1ex  5898  transex  5930  refex  5931  connexex  5933  foundex  5934  extex  5935  symex  5936  ecexg  5969  qsexg  6002  mapexi  6023  map0  6045  mapsn  6046  en2sn  6068  xpsnen  6070  endisj  6072  xpsnen2g  6075  enadj  6080  enpw1lem1  6081  enmap2lem1  6083  enmap1lem1  6089  enpw1pw  6095  enprmaplem1  6096  enprmaplem2  6097  enprmaplem3  6098  enprmaplem5  6100  enprmaplem6  6101  nenpw1pwlem1  6104  lecex  6136  mucex  6154  1cnc  6160  mucid1  6164  ncaddccl  6165  1p1e2c  6176  2p1e3c  6177  tcdi  6185  tc1c  6186  ovcelem1  6192  ceexlem1  6194  ceex  6195  ce0addcnnul  6200  ce0nn  6201  el2c  6212  ce2  6213  leconnnc  6239  tcfnex  6264  nnltp1clem1  6270  nmembers1lem1  6272  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  spacval  6282  fnspac  6283  spacssnc  6284  spacind  6287  nchoicelem3  6291  nchoicelem4  6292  nchoicelem6  6294  nchoicelem7  6295  nchoicelem10  6298  nchoicelem11  6299  nchoicelem14  6302  nchoicelem16  6304  nchoicelem18  6306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741
  Copyright terms: Public domain W3C validator