Theorem snex 4662

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4610. (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 4011	. . 3 |- { A } = { A , A }
2		preq12 4081	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 649	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2491	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4661	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3139	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2511	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 4063	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 197	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4556	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2515	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 167	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1437   e. wcel 1872   _Vcvv 3080   (/)c0 3761   {csn 3998   {cpr 4000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-v 3082  df-dif 3439  df-un 3441  df-nul 3762  df-sn 3999  df-pr 4001

This theorem is referenced by:  prex  4663  elALT  4664  dtruALT2  4665  snelpwi  4666  snelpw  4667  rext  4669  sspwb  4670  intid  4679  moabex  4680  nnullss  4683  exss  4684  opi1  4688  op1stb  4691  opnz  4692  opeqsn  4716  opeqpr  4717  opthwiener  4722  uniop  4723  frirr  4830  frsn  4924  xpsspw  4967  relop  5004  onnev  5562  funopg  5633  fsnex  6196  tpex  6604  snnex  6611  difsnexi  6613  sucexb  6650  soex  6750  elxp4  6751  elxp5  6752  opabex3d  6785  opabex3  6786  1stval  6809  2ndval  6810  fo1st  6827  fo2nd  6828  mpt2exxg  6881  cnvf1o  6906  fnse  6924  suppsnop  6939  brtpos2  6990  wfrlem15  7061  tfrlem12  7118  tfrlem16  7122  mapsn  7524  fvdiagfn  7527  mapsnconst  7528  mapsncnv  7529  mapsnf1o2  7530  ralxpmap  7532  elixpsn  7572  ixpsnf1o  7573  mapsnf1o  7574  ensn1  7643  en1b  7647  mapsnen  7657  xpsnen  7665  endisj  7668  xpsnen2g  7674  domunsncan  7681  enfixsn  7690  domunsn  7731  fodomr  7732  disjenex  7739  domssex2  7741  domssex  7742  map2xp  7751  phplem2  7761  isinf  7794  pssnn  7799  findcard2  7820  ac6sfi  7824  xpfi  7851  fodomfi  7859  pwfilem  7877  fczfsuppd  7910  snopfsupp  7915  fisn  7950  marypha1lem  7956  brwdom2  8097  unxpwdom2  8112  elirrv  8121  epfrs  8223  tc2  8234  tcsni  8235  ranksuc  8344  fseqenlem1  8462  dfac5lem2  8562  dfac5lem3  8563  dfac5lem4  8564  kmlem2  8588  cdafn  8606  cdaval  8607  cdaassen  8619  mapcdaen  8621  cdadom1  8623  cdainf  8629  ackbij1lem5  8661  cfsuc  8694  isfin1-3  8823  hsmexlem4  8866  axcc2lem  8873  dcomex  8884  axdc3lem4  8890  axdc4lem  8892  ttukeylem3  8948  brdom7disj  8966  brdom6disj  8967  fpwwe2lem13  9074  canthwe  9083  canthp1lem1  9084  uniwun  9172  rankcf  9209  nn0ex  10882  hashxplem  12609  hashmap  12611  hashbclem  12619  hashf1lem1  12622  hashge3el3dif  12646  climconst2  13611  incexclem  13893  ramub1lem2  14984  cshwsex  15070  setsvalg  15144  setsid  15163  pwsbas  15384  pwsle  15389  pwssca  15393  pwssnf1o  15395  imasplusg  15417  imasmulr  15418  imasvsca  15420  imasip  15421  xpsc  15462  acsfn  15564  isfunc  15768  homaf  15924  homaval  15925  funcsetcestrclem1  16038  mgm1  16499  sgrp1  16533  mnd1  16576  mnd1OLD  16577  mnd1id  16578  grp1  16757  symg2bas  17038  idrespermg  17051  pmtrsn  17159  psgnsn  17160  abl1  17503  gsum2d2  17605  gsumcom2  17606  dprdz  17662  dprdsn  17668  dprd2da  17674  ring1  17829  pwssplit3  18283  drngnidl  18452  drnglpir  18476  rng1nnzr  18497  evlssca  18744  mpfind  18758  evls1sca  18911  pf1ind  18942  frlmip  19334  islindf4  19394  mattposvs  19478  mat1dimelbas  19494  mat1dimscm  19498  mat1dimmul  19499  mat1rhmval  19502  m1detdiag  19620  mdetrlin  19625  mdetrsca2  19627  mdetrlin2  19630  mdetunilem5  19639  smadiadetglem2  19695  basdif0  19966  ordtbas  20206  leordtval2  20226  dishaus  20396  discmp  20411  concompid  20444  dis2ndc  20473  dislly  20510  dis1stc  20512  unisngl  20540  1stckgen  20567  ptbasfi  20594  dfac14lem  20630  dfac14  20631  ptrescn  20652  xkoptsub  20667  pt1hmeo  20819  xpstopnlem1  20822  ptcmpfi  20826  isufil2  20921  ufileu  20932  filufint  20933  uffix  20934  uffixsn  20938  flimclslem  20997  ptcmplem1  21065  cnextfval  21075  imasdsf1olem  21386  icccmplem1  21838  icccmplem2  21839  rrxip  22347  elply2  23148  plyss  23151  plyeq0lem  23162  taylfval  23312  axlowdimlem15  24984  axlowdim  24989  umgra1  25051  uslgra1  25097  usgra1  25098  usgra1v  25115  cusgra1v  25187  uvtx01vtx  25218  wlkntrl  25290  0pthonv  25309  constr1trl  25316  1pthon  25319  1pthon2v  25321  1conngra  25401  vdgr1d  25629  vdgr1b  25630  vdgr1a  25632  grposn  25941  zrdivrng  26158  0ofval  26426  resf1o  28321  ordtconlem1  28738  esumpr  28895  esumrnmpt2  28897  esumfzf  28898  esum2dlem  28921  esum2d  28922  esumiun  28923  prsiga  28961  rossros  29010  cntnevol  29058  carsgclctunlem1  29157  omsmeas  29163  omsmeasOLD  29164  eulerpartlemgs2  29221  ccatmulgnn0dir  29436  ofs1  29439  ofcs1  29440  bnj918  29585  bnj95  29683  bnj1452  29869  bnj1489  29873  subfacp1lem5  29915  erdszelem5  29926  erdszelem8  29929  cvmliftlem4  30019  cvmliftlem5  30020  cvmlift2lem6  30039  cvmlift2lem9  30042  cvmlift2lem12  30045  fobigcup  30672  elsingles  30690  fnsingle  30691  fvsingle  30692  dfiota3  30695  brapply  30710  brsuccf  30713  funpartlem  30714  altopthsn  30733  altxpsspw  30749  hfsn  30951  neibastop2lem  31021  topjoin  31026  onpsstopbas  31095  bj-sels  31524  bj-snsetex  31525  bj-elsngl  31530  bj-2uplex  31584  bj-elopg  31606  f1omptsnlem  31702  mptsnunlem  31704  topdifinffinlem  31714  finixpnum  31894  ptrest  31903  poimirlem3  31907  poimirlem4  31908  poimirlem28  31932  fdc  32038  heiborlem3  32109  heiborlem8  32114  ismrer1  32134  ldualset  32660  lineset  33272  ispointN  33276  dvaset  34541  dvhset  34618  dibval  34679  dibfna  34691  elrfi  35505  mzpincl  35545  mzpcompact2lem  35562  wopprc  35855  dfac11  35890  kelac2  35893  pwslnmlem1  35920  pwslnm  35922  fvilbdRP  36252  brtrclfv2  36289  frege110  36539  frege133  36562  snelpwrVD  37200  fnchoice  37323  limcresiooub  37663  limcresioolb  37664  cnfdmsn  37699  dvsinax  37723  fourierdlem48  37958  fourierdlem49  37959  sge0sn  38129  sge0p1  38164  sge0xp  38179  nnsum3primesprm  38755  propssopi  38866  funsneqopsn  38886  funsneqop  38887  snstrvtxval  38966  snstriedgval  38967  vtxvalsnop  38970  iedgvalsnop  38971  umgr1op  39016  umgr1opALT  39018  uspgr1op  39102  usgr1op  39103  usgr1vr  39105  mpt2exxg2  39740  mapsnop  39747  lindsrng01  39882  snlindsntorlem  39884  snlindsntor  39885  lmod1lem1  39901  lmod1lem2  39902  lmod1lem3  39903  lmod1lem4  39904  lmod1lem5  39905  lmod1  39906  lmod1zr  39907  aacllem  40161