Theorem snex 4528

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4473. (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 3885	. . 3 |- { A } = { A , A }
2		preq12 3951	. . . . . 6 |- ( ( x = A /\ x = A ) -> { x , x } = { A , A } )
3	2	anidms 645	. . . . 5 |- ( x = A -> { x , x } = { A , A } )
4	3	eleq1d 2504	. . . 4 |- ( x = A -> ( { x , x } e. _V <-> { A , A } e. _V ) )
5		zfpair2 4527	. . . 4 |- { x , x } e. _V
6	4, 5	vtoclg 3025	. . 3 |- ( A e. _V -> { A , A } e. _V )
7	1, 6	syl5eqel 2522	. 2 |- ( A e. _V -> { A } e. _V )
8		snprc 3934	. . . 4 |- ( -. A e. _V <-> { A } = (/) )
9	8	biimpi 194	. . 3 |- ( -. A e. _V -> { A } = (/) )
10		0ex 4417	. . 3 |- (/) e. _V
11	9, 10	syl6eqel 2526	. 2 |- ( -. A e. _V -> { A } e. _V )
12	7, 11	pm2.61i 164	1 |- { A } e. _V

Syntax hints:   -. wn 3   = wceq 1369   e. wcel 1756   _Vcvv 2967   (/)c0 3632   {csn 3872   {cpr 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-un 3328  df-nul 3633  df-sn 3873  df-pr 3875

This theorem is referenced by:  prex  4529  elALT  4530  dtruALT2  4531  snelpwi  4532  snelpw  4533  rext  4535  sspwb  4536  intid  4545  moabex  4546  nnullss  4549  exss  4550  opi1  4554  op1stb  4557  opnz  4558  opeqsn  4582  opeqpr  4583  opthwiener  4588  uniop  4589  frirr  4692  frsn  4904  onnev  4916  xpsspwOLD  4949  relop  4985  funopg  5445  tpex  6374  snnex  6377  difsnexi  6379  sucexb  6415  soex  6516  elxp4  6517  elxp5  6518  opabex3d  6550  opabex3  6551  1stval  6574  2ndval  6575  fo1st  6591  fo2nd  6592  mpt2exxg  6642  cnvf1o  6666  fnse  6684  suppsnop  6699  brtpos2  6746  tfrlem12  6840  tfrlem16  6844  mapsn  7246  fvdiagfn  7249  mapsnconst  7250  mapsncnv  7251  mapsnf1o2  7252  ralxpmap  7254  elixpsn  7294  ixpsnf1o  7295  mapsnf1o  7296  ensn1  7365  en1b  7369  mapsnen  7379  xpsnen  7387  endisj  7390  xpsnen2g  7396  domunsncan  7403  enfixsn  7412  domunsn  7453  fodomr  7454  disjenex  7461  domssex2  7463  domssex  7464  map2xp  7473  phplem2  7483  isinf  7518  pssnn  7523  findcard2  7544  ac6sfi  7548  xpfi  7575  fodomfi  7582  pwfilem  7597  fczfsuppd  7630  snopfsupp  7635  fisn  7669  marypha1lem  7675  brwdom2  7780  unxpwdom2  7795  elirrv  7804  epfrs  7943  tc2  7954  tcsni  7955  ranksuc  8064  fseqenlem1  8186  dfac5lem2  8286  dfac5lem3  8287  dfac5lem4  8288  kmlem2  8312  cdafn  8330  cdaval  8331  cdaassen  8343  mapcdaen  8345  cdadom1  8347  cdainf  8353  ackbij1lem5  8385  cfsuc  8418  isfin1-3  8547  hsmexlem4  8590  axcc2lem  8597  dcomex  8608  axdc3lem4  8614  axdc4lem  8616  ttukeylem3  8672  brdom7disj  8690  brdom6disj  8691  fpwwe2lem13  8801  canthwe  8810  canthp1lem1  8811  uniwun  8899  rankcf  8936  nn0ex  10577  hashge3el3dif  12179  hashxplem  12187  hashmap  12189  hashbclem  12197  hashf1lem1  12200  climconst2  13018  incexclem  13291  ramub1lem2  14080  cshwsex  14119  setsvalg  14189  setsid  14207  pwsbas  14417  pwsle  14422  pwssca  14426  pwssnf1o  14428  imasplusg  14447  imasmulr  14448  imasvsca  14450  imasip  14451  xpsc  14487  acsfn  14589  isfunc  14766  homaf  14890  homaval  14891  symg2bas  15894  idrespermg  15907  gsum2d2  16456  gsumcom2  16457  dprdz  16517  dprdsn  16523  dprd2da  16531  pwssplit3  17122  drngnidl  17291  drnglpir  17315  evlssca  17588  mpfind  17602  evls1sca  17738  pf1ind  17769  frlmip  18183  islindf4  18247  mattposvs  18319  mdetrlin  18389  mdetrsca2  18391  mdetrlin2  18393  mdetunilem5  18402  smadiadetglem2  18458  basdif0  18538  ordtbas  18776  leordtval2  18796  dishaus  18966  discmp  18981  concompid  19015  dis2ndc  19044  dislly  19081  dis1stc  19083  1stckgen  19107  ptbasfi  19134  dfac14lem  19170  dfac14  19171  ptrescn  19192  xkoptsub  19207  pt1hmeo  19359  xpstopnlem1  19362  ptcmpfi  19366  isufil2  19461  ufileu  19472  filufint  19473  uffix  19474  uffixsn  19478  flimclslem  19537  ptcmplem1  19604  cnextfval  19614  imasdsf1olem  19928  icccmplem1  20379  icccmplem2  20380  rrxip  20874  elply2  21644  plyss  21647  plyeq0lem  21658  taylfval  21804  axlowdimlem15  23170  axlowdim  23175  umgra1  23228  uslgra1  23259  usgra1  23260  usgra1v  23276  cusgra1v  23337  uvtx01vtx  23368  wlkntrl  23429  0pthonv  23448  constr1trl  23455  1pthon  23458  1pthon2v  23460  1conngra  23529  vdgr1d  23541  vdgr1b  23542  vdgr1a  23544  grposn  23670  zrdivrng  23887  0ofval  24155  resf1o  25998  gsumle  26214  ordtconlem1  26323  esumpr  26485  esumfzf  26487  prsiga  26543  cntnevol  26611  eulerpartlemgs2  26732  ccatmulgnn0dir  26909  ofs1  26912  ofcs1  26913  subfacp1lem5  27041  erdszelem5  27052  erdszelem8  27055  cvmliftlem4  27146  cvmliftlem5  27147  cvmlift2lem6  27166  cvmlift2lem9  27169  cvmlift2lem12  27172  wfrlem15  27707  fobigcup  27900  elsingles  27918  fnsingle  27919  fvsingle  27920  dfiota3  27923  brapply  27938  brsuccf  27941  funpartlem  27942  altopthsn  27961  altxpsspw  27977  hfsn  28186  onpsstopbas  28246  finixpnum  28385  ptrest  28396  neibastop2lem  28552  topjoin  28557  fdc  28612  heiborlem3  28683  heiborlem8  28688  ismrer1  28708  elrfi  29001  mzpincl  29041  mzpcompact2lem  29059  wopprc  29350  dfac11  29386  kelac2  29389  pwslnmlem1  29416  pwslnm  29418  fnchoice  29722  mpt2exxg2  30698  mapsnop  30705  pmtrsn  30739  psgnsn  30740  mat1dimelbas  30827  mat1dimscm  30831  mat1dimmul  30832  m1detdiag  30865  lindsrng01  30933  snlindsntorlem  30935  snlindsntor  30936  mnd1  30952  grp1  30953  abl1  30954  rng1  30956  rng1nnzr  30957  lmod1lem1  30960  lmod1lem2  30961  lmod1lem3  30962  lmod1lem4  30963  lmod1lem5  30964  lmod1  30965  lmod1zr  30966  snelpwrVD  31496  bnj918  31688  bnj95  31786  bnj1452  31972  bnj1489  31976  bj-sels  32355  bj-snsetex  32356  bj-elsngl  32361  bj-2uplex  32415  bj-elopg  32422  ldualset  32663  lineset  33275  ispointN  33279  dvaset  34542  dvhset  34619  dibval  34680  dibfna  34692