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

Theorem snex 3213
Description: A singleton always exists.
Assertion
Ref Expression
snex

Proof of Theorem snex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 2810 . . . 4
21eleq1d 1960 . . 3
3 ax-sn 3189 . . . 4
4 isset 2304 . . . . 5
5 dfcleq 1889 . . . . . . 7
6 vex 2303 . . . . . . . . . 10
76elsn 2836 . . . . . . . . 9
87bibi2i 301 . . . . . . . 8
98albii 1342 . . . . . . 7
105, 9bitri 237 . . . . . 6
1110exbii 1359 . . . . 5
124, 11bitri 237 . . . 4
133, 12mpbir 197 . . 3
142, 13vtoclg 2351 . 2
15 snprc 2840 . . . 4
1615biimpi 183 . . 3
17 0ex 3212 . . 3
1816, 17syl6eqel 1976 . 2
1914, 18pm2.61i 153 1
Colors of variables: wff set class
Syntax hints:   wn 3   wb 173  wal 1322  wex 1327   wceq 1398   wcel 1400  cvv 2300  c0 2726  csn 2803
This theorem is referenced by:  prex  3214  snelpwg  3216  snelpwi  3218  sspwb  3220  pwadjoin  3221  elopk  3233  el1c  3243  elpw1  3248  elpw12  3249  elpw11c  3251  elpw121c  3252  elpw131c  3253  elpw141c  3254  elpw151c  3255  elpw161c  3256  elpw171c  3257  elpw181c  3258  elpw191c  3259  elpw1101c  3260  elpw1111c  3261  eqpw1  3266  pw111  3274  eluni1g  3276  otkelins2kg  3357  otkelins3kg  3358  opkelcokg  3365  elp6  3367  opksnelsik  3369  elssetkg  3373  opkelimagekg  3375  ins2kss  3383  ins3kss  3384  dfuni12  3395  sikexlem  3399  sikexg  3400  dfimak2  3402  insklem  3408  ins2kexg  3409  ins3kexg  3410  dfuni3  3419  dfint3  3422  setswith  3425  setswithex  3426  ndisjrelk  3427  unipw1  3435  dfpw2  3437  eqpw1uni  3440  dfaddc2  3489  0cex  3500  dfnnc2  3503  nnc0suc  3519  elsuc  3520  nnsucelrlem1  3531  nnsucelr  3535  nndisjeq  3536  preaddccan1lem1  3561  ltfinex  3572  ltfintrilem1  3573  ssfin  3578  ncfinsn  3584  eqpwrelk  3586  eqpw1relk  3587  ncfinraiselem2  3588  ncfinraise  3589  ncfinlowerlem1  3590  ncfinlower  3591  eqtfinrelk  3594  tfinrelkex  3595  tfinsuc  3606  evenfinex  3611  oddfinex  3612  evenoddnnnul  3622  evenodddisjlem1  3623  nnadjoinlem1  3627  nnadjoin  3628  nnadjoinpw  3629  nnpweqlem1  3630  srelk  3632  sfindbl  3638  sfintfinlem1  3639  tfinnnlem1  3641  spfinex  3645  vfinspnn  3649  vfinspss  3659  vfinspclt  3660  vfinncsp  3662  nulnnn  3664  dfop2lem1  3681  opexg  3695  proj2exg  3700  proj2op  3707  setconslem1  3829  setconslem2  3830  setconslem3  3831  setconslem4  3832  setconslem5  3833  setconslem6  3834  setconslem7  3835  df1st2  3836  1stex  3837  dfswap2  3839  swapex  3840  brssetsn  3857  brsi  3859  elimapw1  4136  elimapw12  4137  elimapw13  4138  elimapw11c  4140  elxp4  4318  dmsi  4763  brsnsi  4994  brimage  5013  addcfnex  5043  funsex  5047  crossex  5067  pw1fnex  5069  pw1fnf1o  5072  fullfunexg  5076  clos1ex  5089  transex  5121  refex  5122  connexex  5124  foundex  5125  extex  5126  symex  5127  ecexg  5160  qsexg  5194  mapexi  5215  map0  5237  mapsn  5238  en2sn  5260  xpsnen  5262  endisj  5264  xpsnen2g  5267  enadj  5272  enpw1lem1  5273  enmap2lem1  5275  enmap1lem1  5281  enpw1pw  5287  enprmaplem1  5288  enprmaplem2  5289  enprmaplem3  5290  enprmaplem5  5292  enprmaplem6  5293  nenpw1pwlem1  5296  lecex  5328  mucex  5346  1cnc  5352  mucid1  5356  ncaddccl  5357  1p1e2c  5368  2p1e3c  5369  tcdi  5377  tc1c  5378  ovcelem1  5384  ceexlem1  5386  ceex  5387  ce0addcnnul  5392  ce0nn  5393  el2c  5404  ce2  5405  leconnnc  5431  tcfnex  5456  nnltp1clem1  5462  nmembers1lem1  5464  nncdiv3lem2  5468  nnc3n3p1  5470  spacvallem1  5473  spacval  5474  fnspac  5475  spacssnc  5476  spacind  5479  nchoicelem3  5483  nchoicelem4  5484  nchoicelem6  5486  nchoicelem7  5487  nchoicelem10  5490  nchoicelem11  5491  nchoicelem14  5494  nchoicelem16  5496  nchoicelem18  5498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1323  ax-6 1324  ax-7 1325  ax-gen 1326  ax-8 1402  ax-10 1403  ax-11 1404  ax-12 1405  ax-17 1413  ax-9 1424  ax-4 1429  ax-16 1606  ax-ext 1877  ax-nin 3180  ax-sn 3189
This theorem depends on definitions:  df-bi 174  df-or 356  df-an 357  df-nand 1259  df-ex 1328  df-sb 1568  df-clab 1883  df-cleq 1888  df-clel 1891  df-ne 2014  df-v 2302  df-nin 2613  df-compl 2614  df-in 2615  df-un 2616  df-nul 2727  df-sn 2807
  Copyright terms: Public domain W3C validator