Theorem snex 4112

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.

Step	Hyp	Ref	Expression
1		sneq 3745	. . . 4 ⊢ (x = A → {x} = {A})
2	1	eleq1d 2419	. . 3 ⊢ (x = A → ({x} ∈ V ↔ {A} ∈ V))
3		ax-sn 4088	. . . 4 ⊢ ∃y∀z(z ∈ y ↔ z = x)
4		isset 2864	. . . . 5 ⊢ ({x} ∈ V ↔ ∃y y = {x})
5		axprimlem1 4089	. . . . . 6 ⊢ (y = {x} ↔ ∀z(z ∈ y ↔ z = x))
6	5	exbii 1582	. . . . 5 ⊢ (∃y y = {x} ↔ ∃y∀z(z ∈ y ↔ z = x))
7	4, 6	bitri 240	. . . 4 ⊢ ({x} ∈ V ↔ ∃y∀z(z ∈ y ↔ z = x))
8	3, 7	mpbir 200	. . 3 ⊢ {x} ∈ V
9	2, 8	vtoclg 2915	. 2 ⊢ (A ∈ V → {A} ∈ V)
10		snprc 3789	. . . 4 ⊢ (¬ A ∈ V ↔ {A} = ∅)
11	10	biimpi 186	. . 3 ⊢ (¬ A ∈ V → {A} = ∅)
12		0ex 4111	. . 3 ⊢ ∅ ∈ V
13	11, 12	syl6eqel 2441	. 2 ⊢ (¬ A ∈ V → {A} ∈ V)
14	9, 13	pm2.61i 156	1 ⊢ {A} ∈ V

Syntax hints:  ¬ wn 3   ↔ wb 176  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2860  ∅c0 3551  {csn 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 4079  ax-sn 4088

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 2479  df-ne 2519  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-sn 3742

This theorem is referenced by:  prex  4113  snelpwg  4115  snelpwi  4117  sspwb  4119  pwadjoin  4120  elopk  4130  el1c  4140  elpw1  4145  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  eqpw1  4163  pw111  4171  eluni1g  4173  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  elp6  4264  opksnelsik  4266  elssetkg  4270  opkelimagekg  4272  ins2kss  4280  ins3kss  4281  dfuni12  4292  sikexlem  4296  sikexg  4297  dfimak2  4299  insklem  4305  ins2kexg  4306  ins3kexg  4307  dfuni3  4316  dfint3  4319  setswith  4322  setswithex  4323  ndisjrelk  4324  unipw1  4326  dfpw2  4328  dfaddc2  4382  0cex  4393  dfnnc2  4396  nnc0suc  4413  elsuc  4414  nnsucelrlem1  4425  nnsucelr  4429  nndisjeq  4430  preaddccan2lem1  4455  ltfinex  4465  ltfintrilem1  4466  ssfin  4471  ncfinsn  4477  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinraise  4482  ncfinlowerlem1  4483  ncfinlower  4484  eqtfinrelk  4487  tfinrelkex  4488  tfinsuc  4499  evenfinex  4504  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoin  4521  nnadjoinpw  4522  nnpweqlem1  4523  srelk  4525  sfindbl  4531  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspnn  4542  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  nulnnn  4557  dfop2lem1  4574  opexg  4588  proj2exg  4593  proj2op  4602  phiall  4619  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem5  4736  setconslem6  4737  setconslem7  4738  df1st2  4739  1stex  4740  dfswap2  4742  swapex  4743  brssetsn  4760  brsi  4762  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  elxp4  5109  dmsi  5520  dmep  5525  brsnsi  5774  brimage  5794  composeex  5821  addcfnex  5825  funsex  5829  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  fullfunexg  5860  domfnex  5871  ranfnex  5872  clos1ex  5877  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  ecexg  5950  qsexg  5983  mapexi  6004  map0  6026  mapsn  6027  en2sn  6048  xpsnen  6050  endisj  6052  xpsnen2g  6055  enadj  6061  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  enprmaplem1  6077  enprmaplem2  6078  enprmaplem3  6079  enprmaplem5  6081  enprmaplem6  6082  nenpw1pwlem1  6085  lecex  6116  mucex  6134  1cnc  6140  mucid1  6144  ncaddccl  6145  1p1e2c  6156  2p1e3c  6157  tcdi  6165  tc1c  6166  ovcelem1  6172  ceexlem1  6174  ceex  6175  ce0addcnnul  6180  ce0nn  6181  el2c  6192  ce2  6193  leconnnc  6219  tcfnex  6245  0lt1c  6259  csucex  6260  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  spacval  6283  fnspac  6284  spacssnc  6285  spacind  6288  nchoicelem3  6292  nchoicelem4  6293  nchoicelem6  6295  nchoicelem7  6296  nchoicelem10  6299  nchoicelem11  6300  nchoicelem14  6303  nchoicelem16  6305  nchoicelem18  6307  frecexg  6313  frecxp  6315  dmfrec  6317  fnfreclem2  6319  fnfreclem3  6320  frec0  6322  frecsuc  6323  dmsnfn  6328  scancan  6332