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

Theorem eqeltri 2474
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1  |-  A  =  B
eqeltr.2  |-  B  e.  C
Assertion
Ref Expression
eqeltri  |-  A  e.  C

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2  |-  B  e.  C
2 eqeltr.1 . . 3  |-  A  =  B
32eleq1i 2467 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 201 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eqeltrri  2475  3eltr4i  2483  intab  4040  inex2  4305  pwex  4342  ord3ex  4349  zfpair  4361  opex  4387  otex  4388  uniopel  4420  tpex  4667  unisn2  4670  elvvuni  4897  isarep2  5492  fvex  5701  abrexex2  5960  ovex  6065  oprabex  6146  oprabrexex2  6148  riotaex  6512  tfrlem16  6613  1on  6690  2on  6691  3on  6693  4on  6694  oesuclem  6728  oecl  6740  nnecl  6815  1onn  6841  2onn  6842  3onn  6843  4onn  6844  mapsnf1o2  7020  map1  7144  sbthlem10  7185  map2xp  7236  nnunifi  7317  xpfi  7337  prfi  7340  tpfi  7341  fnfi  7343  pwfi  7360  inf0  7532  cantnffval  7574  cantnfvalf  7576  oemapwe  7606  cantnffval2  7607  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  cnfcom3clem  7618  r1fin  7655  hta  7777  infxpenlem  7851  alephon  7906  alephfplem1  7941  dfac5lem4  7963  dfac5lem5  7964  kmlem10  7995  fin1a2lem10  8245  fin1a2lem12  8247  hsmexlem9  8261  axcc2lem  8272  domtriomlem  8278  axdc2lem  8284  axcclem  8293  brdom7disj  8365  brdom6disj  8366  iundom2g  8371  konigthlem  8399  canthwelem  8481  wunex2  8569  wunex3  8572  nqex  8756  1nq  8761  1pr  8848  axcnex  8978  ax1cn  8980  negex  9260  inelr  9946  cju  9952  nnexALT  9958  2re  10025  3re  10027  4re  10029  5re  10031  6re  10032  7re  10033  8re  10034  9re  10035  10re  10036  2nn  10089  3nn  10090  4nn  10091  5nn  10092  6nn  10093  7nn  10094  8nn  10095  9nn  10096  10nn  10097  nn0ex  10183  zexALT  10256  nneo  10309  zeo  10311  decex  10340  decnncl  10351  deccl  10352  numnncl2  10355  decnncl2  10356  numsucc  10364  numma2c  10371  numadd  10372  numaddc  10373  nummul1c  10374  nummul2c  10375  qexALT  10545  xrex  10565  pnfxr  10669  mnfxr  10670  xnegex  10750  xnegcl  10755  ixxssxr  10884  om2uzuzi  11244  ltweuz  11256  axdc4uzlem  11276  seqex  11280  m1expcl2  11358  faccl  11531  facwordi  11535  faclbnd2  11537  bccl  11568  hashrabrsn  11603  hashunlei  11639  hashpw  11654  s1cli  11712  cats1un  11745  revs1  11752  cats1cli  11776  cats1fvn  11777  crre  11874  remim  11877  climmpt  12320  climle  12388  climsup  12418  sumex  12436  iserabs  12549  isumshft  12574  supcvg  12590  explecnv  12599  geo2lim  12607  ere  12646  eftlub  12665  efsep  12666  tan0  12707  ef01bndlem  12740  divalglem5  12872  divalglem9  12876  sadcf  12920  smupf  12945  crt  13122  phimullem  13123  eulerthlem2  13126  pczpre  13176  pockthi  13230  prmreclem2  13240  igz  13257  0ramcl  13346  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  ndxarg  13444  ressbas  13474  ressbas2  13475  ressid  13479  strle1  13515  topnid  13618  prdsbasex  13629  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdsle  13639  prdsds  13641  prdshom  13644  prdsco  13645  pwselbasb  13665  pwsvscafval  13671  pwssca  13673  pwssnf1o  13675  imassca  13700  imasvsca  13701  imasle  13703  xpslem  13753  xpssca  13758  xpsvsca  13759  isacs2  13833  cidfval  13856  homffval  13872  comfffval  13879  oppchomfval  13895  oppccofval  13897  oppccatid  13900  monfval  13913  oppcmon  13919  sectffval  13931  invffval  13938  isoval  13945  rescbas  13984  reschom  13985  rescco  13987  subccatid  13998  fullsubc  14002  isfunc  14016  isfuncd  14017  idfu2nd  14029  idfu1st  14031  cofu1st  14035  cofu2nd  14037  funcres2c  14053  ressffth  14090  fuccofval  14111  fuchom  14113  fucco  14114  fuccatid  14121  fucid  14123  invfuc  14126  homafval  14139  arwval  14153  idafval  14167  coafval  14174  coapm  14181  setccatid  14194  catchomfval  14208  catccofval  14210  catccatid  14212  xpcbas  14230  xpchomfval  14231  xpccofval  14234  xpccatid  14240  1stf1  14244  1stf2  14245  2ndf1  14247  2ndf2  14248  prf1  14252  prf2fval  14253  evlf2  14270  evlf1  14272  curf1fval  14276  curf11  14278  curf12  14279  curf1cl  14280  curf2  14281  curf2cl  14283  hof2fval  14307  yonedalem4a  14327  yonedalem4c  14329  yonedalem3  14332  yonedainv  14333  isdrs  14346  ispos  14359  isposix  14369  pltfval  14371  lubfval  14390  lubval  14391  lubprop  14392  glbfval  14395  glbval  14396  glbprop  14397  joinfval  14399  joinlem  14402  meetfval  14406  meetlem  14409  clatlem  14494  isglbd  14499  odupos  14517  oduglb  14521  odumeet  14522  odulub  14523  odujoin  14524  ipolt  14540  ipopos  14541  isacs4lem  14549  isdlat  14574  plusffval  14657  issubmnd  14679  ismhm  14695  0mhm  14713  submacs  14720  pwsdiagmhm  14723  gsumvalx  14729  gsumval  14730  gsumress  14732  gsumz  14736  frmdplusg  14754  grpinvfval  14798  grpsubfval  14802  grplactfval  14840  mulgfval  14846  mulgval  14847  issubg  14899  0subg  14920  subgacs  14930  nsgacs  14931  nmznsg  14939  eqgfval  14943  eqgen  14948  isghm  14961  gicen  15019  isga  15023  subgga  15032  orbstafun  15043  orbstaval  15044  orbsta  15045  orbsta2  15046  symgplusg  15054  cayleylem2  15066  cntzfval  15074  cntzval  15075  oppgplusfval  15099  odfval  15126  odval  15127  odinf  15154  dfod2  15155  pgpfi1  15184  pgp0  15185  sylow1lem2  15188  sylow2alem2  15207  sylow2blem1  15209  sylow2blem2  15210  sylow3lem6  15221  lsmfval  15227  lsmvalx  15228  oppglsm  15231  pj1fval  15281  efglem  15303  efgtf  15309  efgsval2  15320  efgsp1  15324  efgrelexlemb  15337  efgcpbllemb  15342  frgpeccl  15348  frgpmhm  15352  vrgpval  15354  frgpuplem  15359  frgpupf  15360  frgpupval  15361  frgpup1  15362  frgpup3lem  15364  frgpnabllem1  15439  frgpnabllem2  15440  iscygodd  15453  prmcyg  15458  lt6abl  15459  dprdfeq0  15535  dmdprdsplitlem  15550  ablfacrplem  15578  ablfacrp  15579  ablfacrp2  15580  ablfac1a  15582  ablfac1b  15583  ablfac1c  15584  ablfac1eu  15586  pgpfaclem2  15595  ablfaclem1  15598  ablfaclem2  15599  ablfaclem3  15600  mgpplusg  15607  mgpress  15614  pwsmgp  15679  opprmulfval  15685  dvdsrval  15705  isunit  15717  unitgrp  15727  unitlinv  15737  unitrinv  15738  dvrfval  15744  isirred  15759  isdrng2  15800  drngmcl  15803  drngid2  15806  issubrg  15823  subrgugrp  15842  isabv  15862  staffval  15890  islmod  15909  scaffval  15923  lssset  15965  islss  15966  lsssn0  15979  lssacs  15998  lspfval  16004  lspval  16006  lspcl  16007  lspuni0  16041  lss0v  16047  0lmhm  16071  lmhmvsca  16076  islbs  16103  islbs3  16182  lbsextlem1  16185  lbsextlem3  16187  lbsextlem4  16188  lbsext  16190  rsp1  16250  drngnidl  16255  2idlval  16259  divsrhm  16263  isnzr2  16289  rrgval  16302  aspval  16342  asclfval  16348  gsumbagdiag  16396  psrbas  16398  psrelbas  16399  psrplusg  16400  psrmulr  16403  psrmulfval  16404  psrmulcllem  16406  psrvscafval  16409  psrvscaval  16411  psrvscacl  16412  psr0cl  16413  psr0lid  16414  psrnegcl  16415  psrlinv  16416  psr1cl  16421  psrlidm  16422  psrridm  16423  psrdi  16425  psrdir  16426  psrass23  16428  resspsradd  16434  resspsrmul  16435  resspsrvsca  16436  mvrval  16440  mvrval2  16441  mplsubglem  16453  mpladd  16460  mplmul  16461  mplvscaval  16466  ressmpladd  16475  ressmplmul  16476  ressmplvsca  16477  subrgmvr  16479  mplmon  16481  mplmonmul  16482  mplcoe1  16483  ltbval  16487  opsrle  16491  opsrtoslem2  16500  mplmon2  16508  psrbag0  16509  psrbagsn  16510  subrgascl  16513  evlslem2  16523  psr1baslem  16538  ressply1add  16579  ressply1mul  16580  ressply1vsca  16581  psropprmul  16587  coe1tmmul2fv  16625  coe1pwmulfv  16627  ply1coe  16639  xrsex  16671  expghm  16732  zrhrhmb  16747  zlmlem  16753  zlmsca  16757  zlmvsca  16758  znle  16772  znbas  16779  znzrhval  16782  zntoslem  16792  znfi  16795  znidomb  16797  znunithash  16800  ipffval  16834  ocvfval  16848  ocvval  16849  elocv  16850  thlbas  16878  thlle  16879  thlleval  16880  thloc  16881  pjfval  16888  pjdm  16889  pjpm  16890  isobs  16902  indistopon  17020  iccordt  17232  concompid  17447  ptbasfi  17566  imastopn  17705  ptcmpfi  17798  uzrest  17882  tmdgsum2  18079  distgp  18082  indistgp  18083  cldsubg  18093  snclseqg  18098  tsmsval  18113  tsmsadd  18129  ustfn  18184  ust0  18202  ustn0  18203  ussid  18243  isusp  18244  ressust  18247  cnextucn  18286  prdsxmetlem  18351  tmslem  18465  nrmmetd  18575  nmfval  18589  tnglem  18634  tngds  18642  tngnm  18645  tngngp2  18646  tngngpd  18647  tngngp  18648  nghmfval  18709  nmo0  18722  cnbl0  18761  remet  18774  re2ndc  18785  xrrest  18791  zcld  18797  icccmp  18809  xrge0gsumle  18817  xrge0tsms  18818  xmetdcn  18822  divcn  18851  expcn  18855  iicon  18870  climcncf  18883  cnmpt2pc  18906  cnrehmeo  18931  cnheiborlem  18932  rellycmp  18935  bndth  18936  evth2  18938  pi1bas  19016  cphsubrglem  19093  cphcjcl  19099  tchex  19129  ipcau2  19144  cncmet  19228  cmsss  19256  ishl2  19277  minveclem4a  19284  minveclem4  19286  finiunmbl  19391  ioombl1lem4  19408  vitalilem4  19456  vitalilem5  19457  ismbf2d  19486  mbfimaopnlem  19500  mbflimsup  19511  mbflim  19513  mbfi1fseqlem6  19565  itgex  19615  bddmulibl  19683  ditgex  19692  recnperf  19745  dv11cn  19838  dvcnvrelem2  19855  ftc1  19879  evlslem3  19888  evlslem1  19889  evlsval2  19894  evl1fval  19900  evl1val  19901  evl1rhm  19902  evl1sca  19903  evl1var  19905  evl1addd  19907  evl1subd  19908  evl1muld  19909  evl1expd  19911  pf1f  19923  pf1mpf  19925  pf1ind  19928  mdegfval  19938  mdegldg  19942  mdegcl  19945  mdegmullem  19954  uc1pval  20015  mon1pval  20017  q1pval  20029  r1pval  20032  ply1remlem  20038  ply1rem  20039  facth1  20040  fta1glem1  20041  fta1glem2  20042  fta1blem  20044  ig1pval  20048  plyeq0lem  20082  quotval  20162  elqaalem3  20191  aaliou3lem4  20216  ulmcau  20264  ulmdvlem1  20269  ulmdvlem3  20271  mbfulm  20275  itgulm  20277  dvradcnv  20290  pserdvlem2  20297  sincn  20313  coscn  20314  tanabsge  20367  reloggim  20446  logcn  20491  dvloglem  20492  logdmopn  20493  dvlog2  20497  cxpcn  20582  cxpcn3  20585  resqrcn  20586  ang180lem3  20606  atanrecl  20704  atan1  20721  atansopn  20725  birthdaylem1  20743  birthday  20746  emcllem4  20790  emcllem6  20792  basellem6  20821  ppiublem1  20939  dchrplusg  20984  dchrmulid2  20989  dchrinvcl  20990  dchrptlem2  21002  dchrsum2  21005  sumdchr2  21007  dchr2sum  21010  bposlem6  21026  bposlem8  21028  lgslem4  21036  lgsdir2lem2  21061  selberglem1  21192  selberglem3  21194  selberg  21195  selbergs  21221  qdrng  21267  usgraexmpl  21373  nbgraf1o0  21409  wlkntrl  21515  0pth  21523  constr1trl  21541  constr2wlk  21551  constr2trl  21552  constr2spth  21553  constr2pth  21554  constr3lem1  21585  constr3trllem3  21592  eupatrl  21643  eupath  21656  konigsberg  21662  gxval  21799  issubgoi  21851  rngoi  21921  dvrunz  21974  isvci  22014  isnvi  22045  imsmetlem  22135  dipfval  22151  sspval  22175  islno  22207  nmooval  22217  nmounbseqi  22231  nmobndseqi  22233  bloval  22235  0ofval  22241  0oval  22242  blocni  22259  ajfval  22263  hmoval  22264  cncph  22273  isph  22276  phpar  22278  ipasslem7  22290  siilem2  22306  ajval  22316  ubthlem1  22325  ubthlem2  22326  minvecolem4b  22333  minvecolem4  22335  minvecolem5  22336  hlex  22353  normlem2  22566  normlem3  22567  normlem6  22570  h0elch  22710  hhsssh  22722  spansnji  23101  nonbooli  23106  3oalem5  23121  3oalem6  23122  3oai  23123  mayetes3i  23185  nmcexi  23482  nmbdfnlb  23506  rnelshi  23515  cnlnadjlem5  23527  pjbdlni  23605  golem2  23728  goeqi  23729  ress0g  24135  ressplusf  24136  ressnm  24137  xrge0tsmsd  24176  rdivmuldivd  24180  rnginvval  24181  dvrcan5  24182  ofldlt1  24196  inftmrel  24203  isinftm  24204  relt  24229  redvr  24230  retos  24231  refld  24232  pstmfval  24244  tpr2tp  24255  tpr2rico  24263  mndpluscn  24265  xrge0pluscn  24279  xrge0mulc1cn  24280  xrge0haus  24283  lmlimxrge0  24287  lmxrge0  24290  qqhval  24311  qqhcn  24328  qqhucn  24329  esumex  24379  esumcst  24408  hasheuni  24428  esumcvg  24429  isrnsigaOLD  24448  prsiga  24467  brsiga  24490  mbfmcnt  24571  sxbrsigalem3  24575  dya2iocuni  24586  dya2iocucvr  24587  sxbrsigalem1  24588  sxbrsiga  24593  sibf0  24602  sibfof  24607  sitgclg  24609  coinflipprob  24690  coinfliprv  24693  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvglem  24777  subfacp1lem1  24818  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  kur14lem7  24851  iiscon  24892  iillyscon  24893  cvmliftlem5  24929  cvmliftlem8  24932  cvmliftlem10  24934  cvmlift2lem9  24951  ghomgrpilem2  25050  ghomsn  25052  ghomgrplem  25053  circum  25064  climlec3  25167  prodfclim1  25174  prodex  25186  binomfallfaclem2  25307  predasetex  25394  trpredex  25454  altopex  25709  colinearex  25898  bpoly4  26009  rankeq1o  26016  ssoninhaus  26102  areacirc  26187  upixp  26321  sdclem2  26336  sdclem1  26337  fdc  26339  lmclim2  26354  caures  26356  idcncf  26359  cncfres  26364  heibor1lem  26408  heiborlem3  26412  heibor  26420  rrnval  26426  rrnmet  26428  reheibor  26438  grpokerinj  26450  isdrngo1  26462  isdrngo2  26464  isrngohom  26471  idlval  26513  isidl  26514  0idl  26525  0rngo  26527  divrngidl  26528  smprngopr  26552  igenval  26561  mapfzcons2  26665  jm2.23  26957  jm2.27dlem2  26971  jm2.27dlem4  26973  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  aomclem6  27024  islssfgi  27038  pwssplit4  27059  pwslnmlem0  27061  frlmbas  27091  frlmbasf  27096  frlmvscafval  27098  uvcvval  27103  uvcvvcl  27104  frlmsslss2  27113  frlmlbs  27117  ellspd  27122  elfilspd  27123  mapfien2  27126  pwfi2en  27129  frlmpwfi  27130  islinds2  27151  lsslindf  27168  lsslinds  27169  islindf4  27176  hbtlem1  27195  hbtlem7  27197  mncn0  27212  aaitgo  27235  symgfisg  27277  psgnfval  27291  cnmsgnsubg  27302  psgnghm  27305  psgnghm2  27306  mndvcl  27314  mamucl  27324  mamudiagcl  27325  mamulid  27326  mamurid  27327  mamuvs1  27331  mamuvs2  27332  matmulr  27335  mdetfval  27355  mendplusgfval  27361  mendmulrfval  27363  mendvscafval  27366  subrgacs  27376  sdrgacs  27377  cntzsdrg  27378  idomrootle  27379  idomodle  27380  deg1mhm  27394  rfcnpre1  27557  fcnre  27563  refsumcn  27568  refsum2cnlem1  27575  clim1fr1  27594  climexp  27598  climinf  27599  climneg  27603  climdivf  27605  itgsin0pilem1  27611  stoweidlem47  27663  stoweidlem53  27669  stoweidlem57  27673  stoweidlem59  27675  wallispilem3  27683  wallispilem4  27684  wallispilem5  27685  wallispi  27686  stirlinglem1  27690  stirlinglem8  27697  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  usgra2adedgwlkon  28047  dpval  28227  bnj105  28795  bnj918  28841  bnj95  28941  bnj852  28998  bnj865  29000  lshpset  29461  lsatset  29473  lcvfbr  29503  islfl  29543  lfl0f  29552  lfl1  29553  lfladd0l  29557  lflnegl  29559  lflvscl  29560  lflvsdi1  29561  lflvsdi2  29562  lflvsdi2a  29563  lflvsass  29564  lfl0sc  29565  lflsc0N  29566  lfl1sc  29567  lkrfval  29570  lkr0f  29577  lkrsc  29580  eqlkr2  29583  ldualvbase  29609  ldualfvadd  29611  ldualvaddval  29614  ldualsca  29615  ldualfvs  29619  ldualvsval  29621  isopos  29663  cmtfvalN  29693  cvrfval  29751  pats  29768  glbconN  29859  llnset  29987  lplnset  30011  lvolset  30054  lineset  30220  isline  30221  pointsetN  30223  psubspset  30226  ispsubsp  30227  pmapfval  30238  pmapval  30239  paddfval  30279  paddval  30280  pclfvalN  30371  pclvalN  30372  polfvalN  30386  polvalN  30387  psubclsetN  30418  ispsubclN  30419  watfvalN  30474  watvalN  30475  lhpset  30477  lautset  30564  islaut  30565  pautsetN  30580  ispautN  30581  ldilfset  30590  ldilset  30591  ltrnfset  30599  ltrnset  30600  dilfsetN  30634  dilsetN  30635  trnfsetN  30637  trlfset  30642  cdleme25cl  30839  cdleme26e  30841  cdleme26eALTN  30843  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme29cl  30859  cdleme31snd  30868  cdleme31fv  30872  cdlemefrs29clN  30881  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32a  30923  cdleme40m  30949  cdleme40n  30950  cdleme42b  30960  cdlemeg46c  30995  tgrpfset  31226  tgrpbase  31228  tgrpopr  31229  tendofset  31240  istendo  31242  tendopl  31258  tendo02  31269  tendoi  31276  erngfset  31281  erngbase  31283  erngfplus  31284  erngfmul  31287  erngfset-rN  31289  erngbase-rN  31291  erngfplus-rN  31292  erngfmul-rN  31295  cdlemk29-3  31393  cdlemk36  31395  cdlemk40  31399  cdlemkid5  31417  cdlemkid  31418  cdlemk56  31453  dvafset  31486  dvasca  31488  dvavbase  31495  dvafvadd  31496  dvafvsca  31498  diaffval  31513  diafval  31514  diaval  31515  dvhfset  31563  dvhsca  31565  dvhvbase  31570  dvhfvadd  31574  dvhfvsca  31583  docaffvalN  31604  docafvalN  31605  docavalN  31606  djaffvalN  31616  djafvalN  31617  djavalN  31618  dibffval  31623  dibfval  31624  dibopelvalN  31626  dibopelval2  31628  dibelval3  31630  diblsmopel  31654  dicffval  31657  dicfval  31658  dicval  31659  cdlemn11a  31690  dihffval  31713  dihfval  31714  dihvalcqpre  31718  dihopelvalcpre  31731  dihord6apre  31739  dihpN  31819  dochffval  31832  dochfval  31833  dochval  31834  djhffval  31879  djhfval  31880  djhval  31881  islpolN  31966  lpolconN  31970  dochpolN  31973  lcfrlem8  32032  lcfrlem9  32033  lcdfval  32071  lcd0vvalN  32096  mapdffval  32109  mapdfval  32110  mapdval  32111  mapd1o  32131  mapdunirnN  32133  mapdhval  32207  mapdhval0  32208  hvmapffval  32241  hvmapfval  32242  hvmapval  32243  hdmap1ffval  32279  hdmap1fval  32280  hdmap1vallem  32281  hdmapffval  32312  hdmapfval  32313  hgmapffval  32371  hgmapfval  32372  hlhilset  32420  hlhilsca  32421  hlhilbase  32422  hlhilplus  32423  hlhilvsca  32433  hlhilip  32434  hlhilnvl  32436  hlhillsm  32442  hlhillcs  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator