Theorem snex 4111

Description: A singleton always exists. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
snex	|- {A} e. _V

Proof of Theorem snex

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sneq 3744	. . . 4 |- (x = A -> {x} = {A})
2	1	eleq1d 2419	. . 3 |- (x = A -> ({x} e. _V <-> {A} e. _V))
3		ax-sn 4087	. . . 4 |- E.yA.z(z e. y <-> z = x)
4		isset 2863	. . . . 5 |- ({x} e. _V <-> E.y y = {x})
5		axprimlem1 4088	. . . . . 6 |- (y = {x} <-> A.z(z e. y <-> z = x))
6	5	exbii 1582	. . . . 5 |- (E.y y = {x} <-> E.yA.z(z e. y <-> z = x))
7	4, 6	bitri 240	. . . 4 |- ({x} e. _V <-> E.yA.z(z e. y <-> z = x))
8	3, 7	mpbir 200	. . 3 |- {x} e. _V
9	2, 8	vtoclg 2914	. 2 |- (A e. _V -> {A} e. _V)
10		snprc 3788	. . . 4 |- (-. A e. _V <-> {A} = (/))
11	10	biimpi 186	. . 3 |- (-. A e. _V -> {A} = (/))
12		0ex 4110	. . 3 |- (/) e. _V
13	11, 12	syl6eqel 2441	. 2 |- (-. A e. _V -> {A} e. _V)
14	9, 13	pm2.61i 156	1 |- {A} e. _V

Syntax hints:  -. wn 3   <-> wb 176  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  _Vcvv 2859  (/)c0 3550  {csn 3737

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

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  4412  elsuc  4413  nnsucelrlem1  4424  nnsucelr  4428  nndisjeq  4429  preaddccan2lem1  4454  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  4601  phiall  4618  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem5  4735  setconslem6  4736  setconslem7  4737  df1st2  4738  1stex  4739  dfswap2  4741  swapex  4742  brssetsn  4759  brsi  4761  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  elxp4  5108  dmsi  5519  dmep  5524  brsnsi  5773  brimage  5793  composeex  5820  addcfnex  5824  funsex  5828  crossex  5850  pw1fnex  5852  pw1fnf1o  5855  fullfunexg  5859  domfnex  5870  ranfnex  5871  clos1ex  5876  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  ecexg  5949  qsexg  5982  mapexi  6003  map0  6025  mapsn  6026  en2sn  6047  xpsnen  6049  endisj  6051  xpsnen2g  6054  enadj  6060  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  enprmaplem1  6076  enprmaplem2  6077  enprmaplem3  6078  enprmaplem5  6080  enprmaplem6  6081  nenpw1pwlem1  6084  lecex  6115  mucex  6133  1cnc  6139  mucid1  6143  ncaddccl  6144  1p1e2c  6155  2p1e3c  6156  tcdi  6164  tc1c  6165  ovcelem1  6171  ceexlem1  6173  ceex  6174  ce0addcnnul  6179  ce0nn  6180  el2c  6191  ce2  6192  leconnnc  6218  tcfnex  6244  0lt1c  6258  csucex  6259  addccan2nclem2  6264  nmembers1lem1  6268  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  frecexg  6312  frecxp  6314  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319  frec0  6321  frecsuc  6322  dmsnfn  6327  scancan  6331