Theorem eqid 1884

Description: Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41.

This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). (Thanks to Stefan Allan for this information.)

Assertion

Ref	Expression
eqid	|- A = A

Proof of Theorem eqid

Step	Hyp	Ref	Expression
1		biid 187	. 2 |- (x e. A <-> x e. A)
2	1	eqriv 1881	1 |- A = A

Syntax hints:   = wceq 1298   e. wcel 1300

This theorem is referenced by:  eqidd 1885  visset 2295  reu6 2443  sbceqal 2502  sbcbii 2506  ssidOLD 2635  uniiunlem 2693  dfnul2 2877  dfnul3 2878  noel 2879  npss0OLD 2912  iforOLD 3009  snidg 3067  prid1g 3104  tpid1 3111  tpid2 3113  tpid3 3116  snsspr1OLD 3136  int0 3230  dfiin2g 3286  syl5eqbr 3370  syl5eqbrr 3371  syl6breq 3376  ssbriOLD 3380  opabbii 3402  so 3620  nlim0OLD 3722  sucidg 3743  ordun 3771  unisn2 3799  euexeqOLD 3826  euexaleq 3827  eufromeq3 3830  ralxfrALT 3840  reuxfr 3847  finds1 3982  relop 4113  ididg 4117  ididgOLD 4118  issetidOLD 4122  dm0OLD 4171  dmiOLD 4173  xpcan 4348  xp11bOLD 4349  xpcan2 4350  xp11aOLD 4351  funfn 4451  f0 4600  dffn4 4623  f1orn 4648  f1oabexg 4650  f1o00 4668  f1o0 4670  funbrfvb 4714  dffn5 4717  funfv 4731  fvco 4736  fvopab4g 4742  fvopab4gf 4744  eqfnfv2 4767  eqfnfv2OLD 4768  eufnfv 4771  fvimacnvALT 4782  fopabcos 4806  fopabsnOLD 4816  funiunfv 4842  oprabbii 4923  oprabval2gf 4955  oprabval3 4959  oprabval6g 4962  mpt2exg 5013  1st2val 5038  2nd2val 5039  curry1 5075  curry1f 5076  curry1val 5077  curry2 5078  curry2f 5079  curry2val 5080  tfr1 5132  tfr2 5133  tfr3 5134  tz7.44-1 5136  rdglem1 5145  0lt1o 5192  oe0m 5202  oawordeu 5237  nneob 5312  ecelqsi 5350  ecoptocl 5362  ecopoprsym 5369  ecopoprtrn 5370  th3qlem2 5374  th3q 5376  en2d 5459  en2 5461  en3 5462  dom2d 5463  dom2 5464  pw2en 5505  ac6sfilem3 5508  sbth 5520  riotabiia 5576  mapen 5585  mapxpen 5589  xpmapenlem4 5593  xpmapen 5595  unbnn 5637  unfilem3 5643  abfii3 5653  iunfi 5659  pwfi 5661  ordtype 5691  hartog 5693  onsdom 5694  inf0 5712  inf3 5726  infeq5 5727  tz9.1 5753  tz9.12 5773  ssrankr1 5787  rankel 5791  rankpw 5795  r1rankid 5805  scott0 5847  cplem2 5851  omsublim 5887  aceq3 5895  aceq4 5896  aceq5 5902  aceq6a 5903  aceq6b 5904  ac6 5917  aceqkm 5943  numth 5946  weth 5949  zorn2lem6 5955  zornlem 5957  zorn2 5958  brdom7disj 5966  brdom6disj 5967  iundom 5974  cardsn 5984  unxpdomlem 5995  alephfp2 6049  dominf 6052  0npi 6162  recidpq 6223  0npr 6248  genpprecl 6256  00sr 6360  opelreal 6401  eqresr 6407  ltsor 6413  pncan3 6534  leid 6701  renfdisjOLD 6713  ltpnf 6717  mnflt 6718  mnfltpnf 6719  xrleid 6735  divcan2i 6905  nnleltp1 7138  0nn0 7322  0z 7355  uzwo3 7431  zmin 7432  znq 7438  fldiv 7497  icoshftf1o 7580  seq11 7730  seq1p1 7731  seq1fn 7733  shftfn 7756  shftval 7759  seqzres2 7804  dfseq0 7806  exp0 7814  0exp 7832  sq0 7880  discrlem2 7907  discrlem 7909  sqrlem21 7943  sqrmsqi 7959  replim 8011  abs0 8129  fz1fi 8229  hashfz1 8232  hashen 8233  fsum1i 8265  fsump1i 8266  climsub 8390  climcmp 8398  caucvg2i 8425  caucvg3i 8427  iserzabsi 8439  cvgcmp2i 8441  cvgcmp2ci 8444  cvgcmp3cei 8448  isumclim5 8463  isumshfti 8465  isumshft2i 8466  isummulc1 8473  isummulc1iALT 8474  infcvgaux1i 8480  infcvgaux2i 8481  infcvgi 8485  explecnv 8495  geolimi 8498  geolim 8499  geolim1i 8500  geolim1 8501  geosumi 8503  geoisum 8504  geoisum1 8506  geoisum1c 8507  cvgratlem5 8516  cvgrati 8517  divccncf 8542  ivthlem8 8550  isupivthi 8552  dsupivthi 8554  efseq1ex 8568  dfef2i 8569  efcl 8574  efcvgfsum 8577  reefcli 8579  erelem2 8582  erelem6 8586  ereALT 8593  ege2 8594  ele3 8595  ege2le3 8596  ef0 8597  efcji 8598  efaddlem23 8622  efaddlem27 8626  efaddlem28 8627  efaddi 8628  eftlex 8640  ef1tlubi 8644  ef01tllem2 8646  ef01tllem2OLD 8647  ef01tlubi 8648  absef01tlubi 8650  eirrlem3 8653  eirr 8656  ef4pi 8664  ef4p 8665  efge1i 8666  efge1pi 8667  absefm1lei 8677  eflegeoi 8680  efcnlem3 8686  reeff1olem2 8690  sin01bndlem2 8734  cos01bndlem2 8736  sin01bnd 8738  cos01bnd 8739  acdc3 8755  acdc2lem2 8758  acdc2 8759  acdc5lem2 8761  acdc5 8762  acdc 8764  acdcALT 8765  nnenom 8767  qnnen 8772  unben 8774  infpn 8777  ruclem15 8793  ruclem38 8816  infxpidmlem9 8829  infxpidm 8833  infmap2 8850  eltopsp 8873  tpsex 8874  istps2 8876  basgen2 8909  ntrval 8952  clsval 8953  0cld 8954  iincld 8955  uncld 8957  cldcls 8958  cls0 8985  ntr0 8986  neival 8993  neii2 8998  neiss 8999  opnneiss 9008  innei 9012  neissex 9014  lpval 9019  qdensere 9027  cnpval 9035  cnpimaex 9041  cnima 9044  cnco 9045  cnpco 9046  cnclima 9048  haustop 9063  dfms2 9076  met0 9092  metres 9100  metxpcl 9109  metxplem4 9110  metxp 9111  blfval 9112  blval 9114  blrn 9118  blf 9121  blelrn 9125  blss 9130  opni 9141  opni2 9142  opni3 9143  blssopn 9144  opnuni 9145  opnin 9146  unirnbl 9152  neibl 9154  lpbl 9157  methausi 9159  methaus 9160  metcnpf 9161  metcnf 9162  metcnconst 9163  metcnp 9165  metcn 9167  metcnss 9176  metcnss2 9177  metidcn 9178  metdnsconst 9179  cncfmet 9183  remetdval 9186  remet 9188  tgioo 9193  rehaus 9195  lmrel 9205  lmbr 9206  lmuni 9229  lmsslem 9230  lmss 9231  caussi 9232  causs 9233  lmfex 9237  cmsmet 9239  metelcls 9243  metcld 9245  metcn4 9249  metcn4i 9250  oprcn 9255  opr1cn 9256  opr2cn 9257  opr1scn 9258  addcn 9264  subcn 9265  mulcn 9266  fsumcnlem 9267  fsumcn 9268  iscms2 9272  lmcau 9274  cmsss 9275  bcthlem32 9308  bcth 9310  grprndm 9334  0ngrp 9335  grprn 9336  grpidval 9342  grprcan 9347  grpinvval 9351  grpinvcl 9352  grpinvid 9358  grplcan 9359  grpasscan1 9361  grpasscan2 9362  grp2inv 9363  grpinvf 9364  grpinvop 9365  grpdivfval 9366  grpdivval 9367  grpdivf 9370  grpdivdiv 9372  grpmuldivass 9373  grpdivid 9374  grppncan 9375  grpnpcan 9376  grppnpcan2 9377  grpnnncan2 9378  gxoprval 9380  gxval 9381  gxpval 9382  gxnval 9383  gx0 9384  gxnn0neg 9386  gxnn0suc 9387  gxcl 9388  gxcom 9392  gxinv 9393  gxsuc 9395  gxid 9396  gxnn0add 9397  gxadd 9398  gxnn0mul 9400  gxmul 9401  resgrprn 9403  grplactval 9405  grplactf1o 9406  ablgrp 9410  abldivdiv4 9417  ablnncan 9420  gxdi 9422  subgres 9426  subgid 9429  subgabl 9432  cnid 9435  addinv 9436  readdsubg 9437  zaddsubg 9438  mulid 9440  ghgrpi 9445  gafo 9451  isga2 9452  ga0 9453  gaid 9454  ssga 9455  gagrp 9456  gaf 9457  gagrpid 9458  gaass 9459  gacan 9460  gapm 9462  ringabl 9475  vcabl 9508  vcm 9522  vcrinv 9523  vclinv 9524  vcoprnelem 9529  vcoprne 9530  vcex 9531  cnvc 9534  nvvop 9560  nvex 9562  nvvc 9566  nvabl 9567  nvsf 9570  nvscl 9579  nvsid 9580  nvsass 9581  nvdi 9583  nvdir 9584  nv2 9585  vsfval 9586  nvzcl 9587  nv0 9590  nvsz 9591  nvinv 9592  invfval 9593  nvmval 9595  nvmfval 9596  nvzs 9597  nvmf 9598  nvnnncan1 9600  nvnnncan2 9601  nvmdi 9602  nvnegneg 9603  nvrinv 9605  nvlinv 9606  nvsubadd 9607  nvpncan2 9608  nvaddsub4 9613  nvsubsub23 9614  nvnncan 9615  nvmeq0 9616  nvmid 9617  nvf 9618  nvdm 9621  nvs 9622  nvsub 9627  nvz0 9628  nvz 9629  nvtri 9630  nvmtri 9631  nvmtri2 9632  nvabs 9633  nvge0 9634  nvop 9637  nvoprne 9638  cnnvg 9640  cnnvba 9641  cnnvdemo 9642  cnnvs 9643  cnnvnm 9644  cnnvm 9645  elimnvu 9647  imsdval2 9650  nvnd 9651  imsdf 9652  imsmet 9656  nvelbl 9657  nvelbl2 9658  nvcnf 9659  nvcnpf 9660  nvcni 9661  nvcni2 9662  nvcni3 9663  nvlmcl 9664  nvlmle 9665  cnims 9666  vacnlem3 9669  vacn 9673  sqcn 9674  sqcn2 9675  nmcni 9677  nmcn 9678  nmcn2 9679  nmcn3 9680  nmcnc 9681  abscn 9682  abscncfALT 9683  va1cnlem 9684  va1cn 9685  sm1cnilem 9686  sm1cni 9687  ipfval 9691  ipval 9692  ipid 9702  ipcl 9704  ipf 9705  ipcj 9706  ip0r 9709  ipz 9711  ip1cnilem2 9713  ip1cnilem3 9714  ip1cnilem4 9715  ip1cnilem5 9716  ip1cni 9718  sspval 9721  sspid 9723  sspnv 9724  sspba 9725  sspg 9726  ssps 9728  sspmlem 9730  sspmval 9731  sspm 9732  sspz 9733  sspn 9734  sspival 9736  sspi 9737  sspimsval 9738  sspims 9739  lnoval 9752  lnof 9755  lno0 9756  lnocoi 9757  lnoadd 9758  lnosub 9759  lnomul 9760  nvcnpi3 9761  nvcnpi4 9762  nvo00 9763  nmoval 9765  nmosetn0 9767  nmoxr 9768  nmoge0 9769  nmorepnf 9770  nmolb 9773  isblo2 9783  bloln 9784  blof 9785  nmblore 9786  0oo 9789  0lno 9790  nmo0 9791  0blo 9792  nmlno0i 9794  nmlno0 9795  nmlnoubi 9796  nmlnogt0 9797  lnon0 9798  nmblolbii 9799  nmblolbi 9800  isblo3i 9801  blometi 9803  blocnilem 9804  blocni 9805  blocn 9807  blocn2 9808  phop 9818  cnph 9819  elimphu 9821  isph 9822  ip0i 9825  ip1i 9827  ip2i 9828  ipdirilem 9829  ipdiri 9830  ipasslem1 9831  ipasslem2 9832  ipasslem6 9836  ipasslem7 9837  ipasslem8 9838  ipasslem9 9839  ipasslem11 9841  ipassi 9842  ipdir 9843  ipass 9846  ipsubdir 9849  siii 9854  sii 9855  sspph 9856  ipblnfi 9857  ip2eqi 9858  ajfuni 9861  ajfun 9862  ajval 9863  bnnv 9868  bnsscmcl 9870  cnbn 9871  ubthlem3 9874  ubthlem4 9875  ubthlem6 9877  ubthlem9 9880  ubthlem11 9882  ubthlem12 9883  ubthlem12OLD 9884  ubthlem13 9885  ubthlem13OLD 9886  ubthlem14 9887  ubthii 9888  ubthi 9889  minveclem1 9890  minveclem2 9891  minveclem3 9892  minveclem9 9898  minveclem16 9905  minveclem21 9910  minveclem23 9912  minveclem28 9917  minveclem29 9918  minveclem33 9922  minvecex 9923  minveclem37 9926  minveceu 9928  minvecex2 9933  hlipgt0 9963  hlcompl 9964  htthlem4 9970  htthlem5 9971  htthlem12 9978  htthi 9979  pstr 9995  spwval2 9996  spwval 10002  spwnex 10004  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  spwpr4c 10009  laps 10013  sincnlem 10015  sincn 10018  coscn 10019  pilem2 10021  pilem3 10022  pilem4 10023  sineq0 10065  sineq0OLD 10066  efghgrpilem 10073  efghgrpi 10074  efifolem1 10076  efifolem4 10079  shftefif1o 10096  eff1oi 10100  eff1o 10102  findcardOLD 10179  elghom 10195  ghomlin 10196  ghomid 10197  symgoprv 10203  symggrpi 10205  symgidi 10206  tx1cn 10223  tx2cn 10224  upxp 10225  uptx 10226  txcn 10227  txcnopab 10228  2txcn 10229  hmeocna 10237  hmeocnb 10238  cnvhmpha 10240  subsp 10244  subcld 10254  subtopmetlem 10255  subtopmet 10256  filesn 10268  filint 10269  fipfil2 10272  emnfil 10273  filintf 10274  oefil2 10275  filfbas 10276  fgf 10283  fbssfg 10285  fgss 10287  fgid 10289  fgfil 10290  filrn 10293  neifil 10302  hausfillim 10303  isfilmap 10308  filmapss 10309  fmf 10310  fmbas 10311  elfilmap 10312  elfilmap3 10314  sflimf 10318  flimfnei 10319  fbaslim 10322  isflimf 10323  cncomp 10331  comptoppr 10332  reldir 10353  dirdm 10354  dirref 10355  dirtr 10356  dirge 10357  tosdir 10358  rngopid 10370  opidon2 10371  isexid2 10372  ismnd2 10392  grpmnd 10393  rnplrnml0 10402  rnplrnml 10404  unmnd 10405  ringidmlem 10409  on1el3 10412  ring1cl 10415  zrdivrng 10418  h2hva 10475  h2hsm 10476  h2hnm 10477  h2hvs 10478  axhcompl 10500  hiidrcl 10594  normlem7 10615  norm-ii.i 10637  hilid 10661  hilvc 10662  hilnormi 10663  hhba 10667  hh0v 10668  hhims 10672  hhims2 10673  hhip 10677  hhph 10678  bcsiHIL 10680  hilmet 10694  hilmetdval 10695  hilmetba 10696  hhhl 10706  hilcms 10707  hilhl 10708  hhssva 10762  hhsssm 10763  hhssnm 10764  hhssabli 10765  hhssnv 10767  hhssnvt 10768  hhsst 10769  hhshsslem1 10770  hhshsslem2 10771  hhsssh 10772  hhsssh2 10773  hhssba 10774  hhssvs 10775  hhssph 10777  hhssims 10778  hhssims2 10779  hhssbn 10784  occllem7 10812  projlem8 10826  projlem10 10828  projlem31 10849  projlem 10850  projlemHIL 10851  pjthlem13 10864  pjthi 10866  pjval 10872  shsva 10917  hosval 11149  hosvalOLD 11150  homval 11151  hodval 11152  hodvalOLD 11153  hfsval 11154  hfmval 11155  pjcompi 11254  mayetes3i 11310  hoaddcl 11321  homulcl 11322  hodseqi 11357  nmopsetretHIL 11428  nmopsetn0 11429  nmfnsetn0 11442  hhlnoi 11463  hhbloi 11465  hh0oi 11466  nmoplb 11468  nmopub2tHIL 11471  nmfnlb 11485  bravalval 11505  brafn 11508  kbop 11514  kbvalval 11515  eigval1 11521  hmopbdopiHIL 11549  nmlnop0iHIL 11558  nmcopexi 11594  nmcfnexi 11623  cnlnadji 11646  nmopadjlei 11658  kbass2 11688  kbass5 11691  leopsq 11700  opsqrlem3 11713  opsqrlem6 11716  hmopidmch 11725  hmopidmpj 11726  stri 11829  hstri 11837  goeqi 11845  irredi 11966  mdsymlem8 11982  mdsymi 11983  cdj3lem2 12007  bnj941 12842  bnj1386 13103  bnj1494 13162  bnj7 13196  bnj66 13203  bnj153 13247  bnj601 13309  bnj893 13324  bnj906 13328  bnj909 13330  bnj940 13339  bnj1029 13382  bnj1124 13424  bnj1127 13429  bnj1147 13432  bnj1188 13451  bnj1204 13459  bnj1246 13462  bnj1248 13464  bnj1256 13467  bnj1259 13469  bnj1302 13485  bnj1311 13491  bnj1318 13493  bnj1326 13496  bnj1321 13498  bnj1384 13512  bnj1413 13523  bnj1414 13525  bnj1415 13527  bnj1420 13531  bnj1451 13542  bnj1453 13545  bnj1493 13558  bnj1496 13559  bnj1522 13578  bnj1543 13579  bnj1544 13580  bnj1545 13581  fz1eqblem 13608  ghomgrpilem2 13629  ghomgrpi 13630  ghomgrplem 13632  ghomgrp 13633  ghomfo 13634  ghomgsg 13636  ghomf1o 13638  cayleylem3 13643  cayleyi 13644  cayleyth 13646  nn0seqcvg 13660  dvdsmul2 13677  divalglem2 13698  divalglem10 13705  divalg 13706  gcd0val 13716  gcdn0cl 13721  gcddvds 13722  dvdslegcd 13723  gcd0id 13729  eucalgcvga 13754  eucalg 13755  mulgcdlem4 13759  mulgcdlem5 13760  mulgcdlem6 13761  frxp 13951  wfr3g 13956  wfr1 13973  wfr2 13974  frr3g 13980  axdense 14027  axfelem8 14038  axfelem9 14039  axfelem11 14041  axfelem15 14045  brtxp 14067  fnbigcup 14075  fvbigcup 14076  elfix 14077  altopelaltxp 14099  oprabex2gpop 14337  fopab2g 14485  prmapcp3 14498  valpr 14499  prjmapcp 14507  cbicplem 14508  cbicp 14509  prjmapcp2 14515  nZdef 14527  domrancur1b 14548  valcurfn1 14552  valcurfn2 14553  valvalcurfn 14554  sege 14595  prltub 14602  ubpar 14603  supdef 14604  mnlmxl2 14611  defse3 14614  supaub 14615  suplub2 14616  geme2 14617  dutos1 14626  istoset2 14628  tolat 14631  tostos 14637  dfdir2 14639  dirpre 14641  latdir 14643  valproemset 14657  fprod1i 14673  fprodp1i 14674  dmrngrp 14699  ablcomgrp 14702  clfsebs 14707  clfsebsg 14708  clfsebs2 14710  fincmpzer 14711  isppm 14715  seqzp2 14716  mgmrddd 14727  ltlga 14729  symgfo 14730  gaplc 14731  gapm2 14732  curgrpact 14735  grpdivone 14736  grpdivfo 14737  grpdrcan 14738  grpdlcan 14739  grpdivzer 14740  fprodneg 14741  fprodsub 14742  trran2 14757  trinv 14759  cmprtr 14760  cmprtr2 14761  prsubrtr 14763  prsubrtr2 14764  rngdmdmrn 14767  rnplrnml3 14768  ununr 14769  multinv 14771  multinvb 14772  mult2inv 14773  rngunval2 14774  fldax1 14777  fldax2 14778  fldax3 14779  fldax4 14780  fldax5 14781  fldax7 14783  vecax1 14796  vecax2 14797  vecax3 14798  vecax4 14799  vecax5 14800  vecax6 14801  claddinvvec 14803  vec2inv 14804  dblsubvec 14817  mvecrtol2 14820  mulveczer 14822  mulinvsca 14823  muldisc 14824  svli2 14826  svs2 14829  svs3 14830  topindis 14859  unint2t 14866  intfmu2 14867  cnrsfin 14868  cnrscoa 14869  mapdiscnlem 14870  nsn 14874  cmphmp 14878  cnvhmphb 14880  cnvhmph 14881  hmphsyma 14882  hmphre 14884  hmeogrp 14892  homcard 14893  top2ind 14897  subtopsin2 14907  ptincpw 14912  ttcn 14913  intcont 14914  usptoplem 14917  istopx 14918  prtoptop 14919  fgsb 14921  filint2 14923  fgsb2 14925  rcfpfil 14934  limfillem2 14939  limfilnei 14943  conttnf 14944  conttnf2 14945  cnpfillim4 14947  dtopcl 14948  t2t1 14949  dtt2 14951  topgrpbs 14974  topgrpcn 14975  topgrpgrp 14976  topgrptop 14977  idtrgrp 14978  invtrgrp 14979  extopgrp 14980  topgrpsubcnlem 14981  topgrpsubcn 14982  trhom 14983  tpgprop2 14987  cntrsetlem 14999  trnij 15015  cnvtr 15016  mpinf 15027  miminf 15028  lvsovso 15038  supexr 15043  supbrr 15048  doma 15075  coda 15076  ida 15077  cmppfa 15079  dcsda 15080  1ded 15085  dedalg 15090  idosd 15091  cmppfd 15092  domcmpd 15093  codcmpd 15094  rdmob 15095  rcmob 15096  aidm2 15097  dmrngcmp 15098  0ded 15104  0cat 15105  catded 15111  cmpasso 15120  cmpidb 15122  dmo 15123  cdmo 15124  jdmo 15125  cmpmorp 15126  morcat 15127  cmppfc1 15128  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualded 15132  dualcat2 15133  ishomd 15139  ehm 15140  dehm 15141  cehm 15142  mrdmcd 15143  eqidob 15144  homib 15145  hine 15146  cmphmia 15147  cmphmib 15148  iri 15149  cmpassoh 15150  homgrf 15151  imonclem 15162  ismonc 15163  idmon 15166  immon 15167  iepiclem 15172  isepic 15173  cinvlem2 15177  fmamo 15184  vidfunid 15185  iddvvidd 15186  idcvvidc 15187  fmp 15188  idfisf 15189  catsbc 15197  obsubc2 15198  idsubc 15199  domsubc 15200  codsubc 15201  subctct 15202  morsubc 15203  cmpsubc 15204  idsubidsup 15205  idsubfun 15206  dfiin2gOLD 15356  fictblem 15370  fictb 15371  ordtypeOLD 15382  hartogOLD 15384  onsdomOLD 15385  omsublimOLD 15396  opncldf2 15403  opnnei 15417  neiin 15418  hmeoclda 15421  subsubtop 15423  subcls 15424  subntr 15425  cnsubsp 15426  cnsubsp2 15427  compsublem 15430  compsub 15431  cptclsscpt 15432  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  dfcon2 15442  connsub 15443  cnconn 15444  conntoppr 15445  reconnlem4 15449  reconnlem5 15450  reconn 15451  ivthALT 15454  1stctop 15470  2ndc1stc 15477  fnessex 15484  fneuni 15485  refssex 15490  fneref 15493  refref 15494  fnetr 15495  reftr 15497  topfneec 15501  fnessref 15503  refssfne 15504  finptfin 15507  locfintop 15510  locfinnei 15512  lfinpfin 15513  locfincomp 15514  locfincf 15516  comppfsc 15517  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topmtcl 15525  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  t0top 15540  t1top 15544  t1t0 15547  regtop 15549  isnrm2 15552  neifg 15559  supfil 15560  isufil2 15565  ufilfil 15566  filssufillem 15570  filssufil 15571  ufileu 15573  filufint 15574  uffixfr 15575  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  neiplim 15586  limfilcf 15587  flimcls 15588  cnpfillim 15589  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  fmufil 15599  filfm 15600  flimfcnp 15602  sfcls 15604  fclusbas 15610  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  uffclsflim 15616  fcluscnplem 15617  fcluscnp 15618  fcluscomplem 15620  fcluscomp 15621  ufcomp 15622  sfclusf 15624  isfclusf 15625  flfssfcf 15629  uffcfflf 15630  fclsfcnp 15631  tailf 15633  istail 15634  tailmap 15636  filnetlem1 15640  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  filnet 15645  cover2g 15674  fvopabf4g 15703  f1elima 15719  upixp 15729  eroprv 15734  fimax 15746  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  fsumltisumi 15823  isumshft2 15830  subspcld2 15839  subspabs 15840  neificl 15841  blssp 15844  stioo 15845  mettrifi2 15848  geomcau 15849  metdcn 15853  iitop 15867  iiuni 15868  dfii3 15870  iccst 15875  icoopnst 15876  iocopnst 15877  lincmb01cmp 15878  constcncf 15882  cncfco 15887  cnimass 15888  cnres 15889  cnres2 15890  cnresima 15891  cnss 15892  paste 15893  piececn 15894  cncfres 15895  hmeocn 15897  hmeocnv 15898  hmeoopn 15899  hmeocld 15900  tlmbr 15904  lmtlm 15908  txtopi 15909  txunii 15910  txcnoprab 15911  txsubsp 15912  txopn 15913  txcld 15914  cnresoprab 15915  cnopropabco 15917  cnopropabcoc 15918  cnoproprabco 15919  cnoproprabcoc 15920  cnoprab1 15921  cnoprab2 15922  cnoprab1c 15923  cnoprab2c 15924  txmet 15925  txcc 15926  addcntx 15927  subcntx 15928  mulcntx 15929  totbndmet 15935  sstotbnd 15936  totbndss 15937  bndss 15942  blbnd 15943  totbndbnd 15944  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtybndlem 15952  ismtyres 15954  heiborlem1 15955  heiborlem18 15972  heiborlem23 15977  heiborlem33 15987  heiborlem40 15994  heiborlem42 15996  bfplem1 15998  bfplem2 15999  bfplem3 16000  bfplem8 16005  bfplem11 16008  bfp 16009  recms 16010  rrnval 16013  rrnmval 16014  rrndm 16015  rrnmet 16016  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  rrnheibor 16023  reheibor 16025  iccbnd 16026  icccmp 16027  iicmp 16028  exidcl 16029  exidres 16031  exidresid 16032  isgrpda 16033  isablda 16035  ghomco 16040  ghomdiv 16041  grpkerinj 16042  phtpyval 16047  phtpyid 16049  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  isphtpc 16059  phtpcdm 16061  phtpcer 16062  reparphtlem2 16064  reparpht 16065  pcofval 16072  pcoval 16073  pcoval1 16074  pcoval2 16075  pcocn 16076  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  elpi1i 16090  pi1fval 16092  pi1f 16093  pi1val 16094  pi1gp 16095  isringd 16097  ringnegmn1l 16102  ringnegmn1r 16103  ringneglmul 16104  ringnegrmul 16105  ringsubdi 16106  ringsubdir 16107  divrngcl 16110  isdivrng2 16111  rnghomf 16120  rnghom1 16122  rnghomadd 16123  rnghommul 16124  rnggrphom 16125  rnghomco 16128  rngkerinj 16129  rngisohom 16134  rngisocnv 16135  rngisoco 16136  iscringd 16147  fldcrng 16152  crnghomfo 16154  idlss 16164  idl0cl 16166  idladdcl 16167  idllmulcl 16168  idlrmulcl 16169  idlnegcl 16170  idlsubcl 16171  rngidl 16172  0idl 16173  divrngidl 16176  intidl 16177  unichnidl 16179  keridl 16180  pridlidl 16183  pridlnr 16184  pridl 16185  maxidlidl 16189  maxidln1 16192  prrngrng 16199  divrngpr 16201  igenmin 16212  igenidl2 16213  prnc 16215  isfldidl2 16217  dmnnzd 16223  dmncan1 16224  hgrablkne0 16295  emhgrat 16297  ltfrn 16438  fnelstr 16717  stb2strx 16747  stb2v1x 16748  stb2v2x 16749  stb3strx 16754  stb3v1x 16755  stb3v2x 16756  stb3v3x 16757  poslem 16774  isposiNEW 16778  pltne 16783  pltirr 16784  pltnlt 16788  pltn2lp 16789  plttr 16790  posgelem 16795  lubval 16804  glbval 16809  glbvalle 16811  glbprople 16812  joinval 16815  joinval2 16816  meetval 16822  meetval2 16823  joincomALT 16828  meetcomALT 16830  p0le 16845  ple1 16846  latpos 16851  latjcl 16852  latmcl 16853  latjidm 16869  latmle1 16871  latmle2 16872  latlem12 16873  latmidm 16881  latabs1 16882  latabs2 16883  lubsn 16885  latjass 16886  clatlubcl 16890  clatglbcl 16891  clatlat 16893  lubun 16899  lubunNEW 16900  isopi 16910  opposet 16912  oposlem 16913  op0cl 16914  op1cl 16915  glb0 16920  opoccl 16921  opococ 16922  oplecon3 16926  opoc1 16929  opoc0 16930  opltcon3b 16931  opexmid 16934  opnoncon 16935  olj01 16944  oldmm1 16946  olmass 16954  olm0 16958  omlol 16961  omllaw3 16966  omllaw4 16967  omllaw5 16968  cmtcomlem 16969  cmt2 16971  cmtbr3 16975  lecmt 16977  omlfh1 16978  omlfh3 16979  cvrcon3b 16994  cvrle 16995  cvrnbtwn4 16996  cvrnle 16997  cvrne 16998  atombase 17003  leatom 17005  atomn0 17006  atomnle0 17007  atomcmp 17008  atnlt 17009  atomcvreq0 17010  atncvr 17011  atlatlat 17014  hllem1 17020  glbcon 17028  atomnlej1 17030  atomnlej2 17031  atmnem0 17032  hlsuprexch 17033  hlsupr 17036  hlhght4 17037  hl0lt1 17039  hl1atom 17040  hlatexchb1 17043  hlatexchb2 17044  hlatexch1 17045  hlatexch2 17046  hlatmstc 17047  hlatle 17048  hlrelat2 17052  hl2atom 17053  cvr1 17054  cvr2 17055  cvrp 17056  atcvr1 17057  atcvr2 17058  cvrexchlem 17059  cvrexch 17060  cvratlem 17061  cvrat 17062  cvrntr 17063  atcvr0eq 17064  atcvrj0 17065  cvrat2 17066  atcvrne 17067  atcvrj1 17068  atcvrj2b 17069  atlene 17071  atltcvr 17072  atexchcvr 17073  atexchlt 17074  cvrat3 17075  cvrat4 17076  ps-1 17078  ps2 17079  grplem1 17105  grplidinvNEW 17108  isgrpiNEW 17115  grpidclNEW 17118  grprcanNEW 17122  grpinvvalNEW 17126  grpinvclNEW 17127  grpinvidNEW 17133  grplcanNEW 17134  ablgrpNEW 17137  ringiNEW 17143  ringclNEW 17144  ringassNEW 17145  ringideuNEW 17146  ringidcl 17150  ringablNEW 17151  ringlzNEW 17156  ringrzNEW 17157  divrngring 17161  divrngmclNEW 17164  divrngidlemNEW 17165  divrngidNEW 17166  divrngunzNEW 17167  invrcl 17171  plusssval 17205  ocvval 17207  atompoint 17224  0psub 17230  pointpsub 17231  linepsub 17232  atpsub 17233  psubssat 17234  pmapval 17237  pmapssat 17239  pmapssba 17240  pmaple 17241  pmap11 17242  pmapat 17243  pmap0 17245  pmap1 17247  isline2 17248  linepmap 17249  pmapsub 17250  pmapglbx 17251  pmapglb2 17253  pmapglb2x 17254  pmapmeet 17255  paddval 17259  elpaddn0 17261  paddunss 17269  elpadd0 17270  padd01 17272  padd02 17273  paddcom 17274  paddssat 17275  sspadd1 17276  sspadd2 17277  paddss1 17278  paddss2 17279  paddasslem2 17282  paddasslem5 17285  paddasslem12 17292  paddasslem13 17293  paddasslem18 17298  paddidm 17302  paddcl 17303  pmodi 17309  pmodl42 17312  pmapjoin 17313  pmapjat 17314  polval 17318  polval2 17319  polsub 17320  polssat 17321  pol0 17322  pol1 17323  polpmap 17324  2polpmap 17325  2polval 17326  2polss 17327  3pol 17328  polcon3OLD 17329  polcon3 17330  pmaplub 17334  sspmaplub 17335  2pmaplub 17336  paddun 17337  poldmj1 17338  pmapj2 17339  pmapocj 17340  polat 17341  2polat 17342  pnonsing 17343  psubcli2 17349  psubclssat 17350  pmapidcl 17351  0psubcl 17352  1psubcl 17353  atpsubcl 17354  pmapsubcl 17355  ispsubcl2 17356  psubclin 17357  paddatcl 17358  linepsubcl 17359  polsubcl 17360  poml4 17361  poml6 17363  osumcllem1 17364  osumcllem11 17374  osumcl 17375  pmapojoin 17376  pexmid 17377  pexmidlem6 17383  pexmidlem8 17385  psubclsub 17387  watomval 17393  dilset 17402  trnset 17405  pl42lem1 17407  pl42lem2 17408  pl42lem3 17409  pl42lem4 17410  pl42 17411

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-cleq 1877

Copyright terms: Public domain