Theorem snex 4521

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4466. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)

Assertion

Ref	Expression
snex	|- { A } e. _V

Proof of Theorem snex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsn2 3878	. . 3 |- { A } = { A , A }
2		preq12 3944	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 638	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2499	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4520	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3019	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2517	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 3927	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 194	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4410	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2521	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 164	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1362   e. wcel 1755   _Vcvv 2962   (/)c0 3625   {csn 3865   {cpr 3867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-un 3321  df-nul 3626  df-sn 3866  df-pr 3868

This theorem is referenced by:  prex  4522  elALT  4523  dtruALT2  4524  snelpwi  4525  snelpw  4526  rext  4528  sspwb  4529  intid  4538  moabex  4539  nnullss  4542  exss  4543  opi1  4547  op1stb  4550  opnz  4551  opeqsn  4575  opeqpr  4576  opthwiener  4581  uniop  4582  frirr  4684  frsn  4896  onnev  4908  xpsspwOLD  4941  relop  4977  funopg  5438  tpex  6368  snnex  6371  difsnexi  6373  sucexb  6409  soex  6510  elxp4  6511  elxp5  6512  opabex3d  6544  opabex3  6545  1stval  6568  2ndval  6569  fo1st  6585  fo2nd  6586  mpt2exxg  6636  cnvf1o  6660  fnse  6678  suppsnop  6693  brtpos2  6740  tfrlem12  6834  tfrlem16  6838  mapsn  7242  fvdiagfn  7245  mapsnconst  7246  mapsncnv  7247  mapsnf1o2  7248  ralxpmap  7250  elixpsn  7290  ixpsnf1o  7291  mapsnf1o  7292  ensn1  7361  en1b  7365  mapsnen  7375  xpsnen  7383  endisj  7386  xpsnen2g  7392  domunsncan  7399  enfixsn  7408  domunsn  7449  fodomr  7450  disjenex  7457  domssex2  7459  domssex  7460  map2xp  7469  phplem2  7479  isinf  7514  pssnn  7519  findcard2  7540  ac6sfi  7544  xpfi  7571  fodomfi  7578  pwfilem  7593  fczfsuppd  7626  snopfsupp  7631  fisn  7665  marypha1lem  7671  brwdom2  7776  unxpwdom2  7791  elirrv  7800  epfrs  7939  tc2  7950  tcsni  7951  ranksuc  8060  fseqenlem1  8182  dfac5lem2  8282  dfac5lem3  8283  dfac5lem4  8284  kmlem2  8308  cdafn  8326  cdaval  8327  cdaassen  8339  mapcdaen  8341  cdadom1  8343  cdainf  8349  ackbij1lem5  8381  cfsuc  8414  isfin1-3  8543  hsmexlem4  8586  axcc2lem  8593  dcomex  8604  axdc3lem4  8610  axdc4lem  8612  ttukeylem3  8668  brdom7disj  8686  brdom6disj  8687  fpwwe2lem13  8797  canthwe  8806  canthp1lem1  8807  uniwun  8895  rankcf  8932  nn0ex  10573  hashge3el3dif  12171  hashxplem  12179  hashmap  12181  hashbclem  12189  hashf1lem1  12192  climconst2  13010  incexclem  13282  ramub1lem2  14071  cshwsex  14110  setsvalg  14180  setsid  14198  pwsbas  14408  pwsle  14413  pwssca  14417  pwssnf1o  14419  imasplusg  14438  imasmulr  14439  imasvsca  14441  imasip  14442  xpsc  14478  acsfn  14580  isfunc  14757  homaf  14881  homaval  14882  symg2bas  15883  idrespermg  15896  gsum2d2  16440  gsumcom2  16441  dprdz  16501  dprdsn  16507  dprd2da  16515  pwssplit3  17064  drngnidl  17233  drnglpir  17257  frlmip  18045  islindf4  18109  mattposvs  18181  mdetrlin  18251  mdetrsca2  18253  mdetrlin2  18255  mdetunilem5  18264  smadiadetglem2  18320  basdif0  18400  ordtbas  18638  leordtval2  18658  dishaus  18828  discmp  18843  concompid  18877  dis2ndc  18906  dislly  18943  dis1stc  18945  1stckgen  18969  ptbasfi  18996  dfac14lem  19032  dfac14  19033  ptrescn  19054  xkoptsub  19069  pt1hmeo  19221  xpstopnlem1  19224  ptcmpfi  19228  isufil2  19323  ufileu  19334  filufint  19335  uffix  19336  uffixsn  19340  flimclslem  19399  ptcmplem1  19466  cnextfval  19476  imasdsf1olem  19790  icccmplem1  20241  icccmplem2  20242  rrxip  20736  evlssca  21374  mpfind  21396  pf1ind  21406  elply2  21549  plyss  21552  plyeq0lem  21563  taylfval  21709  axlowdimlem15  23025  axlowdim  23030  umgra1  23083  uslgra1  23114  usgra1  23115  usgra1v  23131  cusgra1v  23192  uvtx01vtx  23223  wlkntrl  23284  0pthonv  23303  constr1trl  23310  1pthon  23313  1pthon2v  23315  1conngra  23384  vdgr1d  23396  vdgr1b  23397  vdgr1a  23399  grposn  23525  zrdivrng  23742  0ofval  24010  resf1o  25855  gsumle  26098  ordtconlem1  26208  esumpr  26370  esumfzf  26372  prsiga  26428  cntnevol  26496  eulerpartlemgs2  26611  ccatmulgnn0dir  26788  ofs1  26791  ofcs1  26792  subfacp1lem5  26920  erdszelem5  26931  erdszelem8  26934  cvmliftlem4  27025  cvmliftlem5  27026  cvmlift2lem6  27045  cvmlift2lem9  27048  cvmlift2lem12  27051  wfrlem15  27585  fobigcup  27778  elsingles  27796  fnsingle  27797  fvsingle  27798  dfiota3  27801  brapply  27816  brsuccf  27819  funpartlem  27820  altopthsn  27839  altxpsspw  27855  hfsn  28064  onpsstopbas  28124  finixpnum  28258  ptrest  28269  neibastop2lem  28425  topjoin  28430  fdc  28485  heiborlem3  28556  heiborlem8  28561  ismrer1  28581  elrfi  28875  mzpincl  28915  mzpcompact2lem  28933  wopprc  29224  dfac11  29260  kelac2  29263  pwslnmlem1  29290  pwslnm  29292  fnchoice  29596  mpt2exxg2  30572  mapsnop  30579  pmtrsn  30601  psgnsn  30602  lindsrng01  30711  snlindsntorlem  30713  snlindsntor  30714  mnd1  30730  grp1  30731  abl1  30732  rng1  30734  rng1nnzr  30735  lmod1lem1  30738  lmod1lem2  30739  lmod1lem3  30740  lmod1lem4  30741  lmod1lem5  30742  lmod1  30743  lmod1zr  30744  snelpwrVD  31269  bnj918  31461  bnj95  31559  bnj1452  31745  bnj1489  31749  bj-sels  32038  bj-snsetex  32039  bj-elsngl  32044  bj-2uplex  32098  bj-elopg  32102  ldualset  32343  lineset  32955  ispointN  32959  dvaset  34222  dvhset  34299  dibval  34360  dibfna  34372