MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snex Unicode version

Theorem snex 4110
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4090. (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
StepHypRef Expression
1 dfsn2 3558 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3612 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 629 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2319 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4109 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2781 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2337 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3599 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 188 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4047 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2341 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 158 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5    = wceq 1619    e. wcel 1621   _Vcvv 2727   (/)c0 3362   {csn 3544   {cpr 3545
This theorem is referenced by:  prex  4111  elALT  4112  dtruALT2  4113  snelpwi  4114  snelpw  4115  rext  4116  sspwb  4117  intid  4125  moabex  4126  nnullss  4128  exss  4129  opi1  4133  opnz  4135  opeqsn  4155  opeqpr  4156  opthwiener  4161  uniop  4162  frirr  4263  tpex  4410  snnex  4415  op1stb  4460  sucexb  4491  frsn  4667  onnev  4677  xpsspwOLD  4705  relop  4741  soex  5029  elxp4  5066  elxp5  5067  funopg  5144  opabex3  5621  1stval  5976  2ndval  5977  fo1st  5991  fo2nd  5992  mpt2exxg  6047  cnvf1o  6069  fnse  6084  brtpos2  6092  tposexg  6100  tfrlem12  6291  tfrlem16  6295  mapsn  6695  fvdiagfn  6698  mapsnconst  6699  mapsncnv  6700  mapsnf1o2  6701  elixpsn  6741  ixpsnf1o  6742  mapsnf1o  6743  ensn1  6810  en1b  6814  mapsnen  6823  xpsnen  6831  endisj  6834  xpsnen2g  6840  domunsncan  6847  domunsn  6896  fodomr  6897  disjenex  6904  domssex2  6906  domssex  6907  map2xp  6916  phplem2  6926  isinf  6961  pssnn  6966  findcard2  6983  ac6sfi  6986  xpfi  7013  fodomfi  7020  pwfilem  7034  fisn  7064  marypha1lem  7070  brwdom2  7171  unxpwdom2  7186  elirrv  7195  epfrs  7297  tc2  7311  tcsni  7312  ranksuc  7421  fseqenlem1  7535  dfac5lem2  7635  dfac5lem3  7636  dfac5lem4  7637  kmlem2  7661  cdafn  7679  cdaval  7680  cdaassen  7692  mapcdaen  7694  cdadom1  7696  cdainf  7702  ackbij1lem5  7734  cfsuc  7767  isfin1-3  7896  hsmexlem4  7939  axcc2lem  7946  dcomex  7957  axdc3lem4  7963  axdc4lem  7965  ttukeylem3  8022  brdom7disj  8040  brdom6disj  8041  fpwwe2lem13  8144  canthwe  8153  canthp1lem1  8154  uniwun  8242  rankcf  8279  nn0ex  9850  hashxplem  11262  hashmap  11264  hashbclem  11267  hashf1lem1  11270  climconst2  11899  ramub1lem2  12948  setsvalg  13045  setsid  13061  pwsbas  13260  pwsle  13265  pwssca  13269  pwssnf1o  13271  imasplusg  13294  imasmulr  13295  imasvsca  13297  xpsc  13333  acsfn  13405  isfunc  13582  homaf  13706  homaval  13707  gsum2d2  15060  gsumcom2  15061  dprdz  15100  dprdsn  15106  dprd2da  15112  drngnidl  15813  drnglpir  15837  basdif0  16523  ordtbas  16754  leordtval2  16774  dishaus  16942  discmp  16957  concompid  16989  dis2ndc  17018  dislly  17055  dis1stc  17057  1stckgen  17081  ptbasfi  17108  dfac14lem  17143  dfac14  17144  ptrescn  17165  xkoptsub  17180  pt1hmeo  17329  xpstopnlem1  17332  ptcmpfi  17336  isufil2  17435  ufileu  17446  filufint  17447  uffix  17448  uffixsn  17452  flimclslem  17511  ptcmplem1  17578  imasdsf1olem  17769  icccmplem1  18159  icccmplem2  18160  evlssca  19238  mpfind  19260  pf1ind  19270  elply2  19410  plyss  19413  plyeq0lem  19424  taylfval  19570  grposn  20712  zrdivrng  20929  0ofval  21195  subfacp1lem5  22886  erdszelem5  22897  erdszelem8  22900  cvmliftlem4  22990  cvmliftlem5  22991  cvmlift2lem6  23010  cvmlift2lem9  23013  cvmlift2lem12  23016  umgra1  23049  vdgr1d  23065  vdgr1b  23066  vdgr1a  23068  wfrlem15  23438  fobigcup  23615  elsingles  23631  fnsingle  23632  fvsingle  23633  brapply  23651  funpartfv  23657  altopthsn  23669  altxpsspw  23685  axlowdimlem15  23758  axlowdim  23763  hfsn  23983  onpsstopbas  24043  cbicp  24332  basexre  24688  1alg  24888  1ded  24904  1cat  24925  vtare  25051  smbkle  25209  neibastop2lem  25475  topjoin  25480  fdc  25621  heiborlem3  25703  heiborlem8  25708  ismrer1  25728  ralxpmap  25927  elrfi  25935  mzpincl  25978  mzpcompact2lem  25995  wopprc  26289  dfac11  26326  kelac2  26329  pwssplit3  26356  pwslnmlem1  26360  pwslnm  26362  enfixsn  26423  islindf4  26474  snelpwrVD  27296  bnj918  27485  bnj95  27585  bnj153  27601  bnj1452  27771  bnj1489  27775  lsatset  27981  ldualset  28116  lineset  28728  ispointN  28732  dvaset  29995  dvhset  30072  dibval  30133  dibfna  30145
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-un 3083  df-nul 3363  df-sn 3550  df-pr 3551
  Copyright terms: Public domain W3C validator