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

Theorem eqeltri 2506
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 2499 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 201 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eqeltrri  2507  3eltr4i  2515  intab  4080  inex2  4345  pwex  4382  ord3ex  4389  zfpair  4401  opex  4427  otex  4428  uniopel  4460  tpex  4708  unisn2  4711  elvvuni  4938  isarep2  5533  fvex  5742  abrexex2  6001  ovex  6106  oprabex  6187  oprabrexex2  6189  riotaex  6553  tfrlem16  6654  1on  6731  2on  6732  3on  6734  4on  6735  oesuclem  6769  oecl  6781  nnecl  6856  1onn  6882  2onn  6883  3onn  6884  4onn  6885  mapsnf1o2  7061  map1  7185  sbthlem10  7226  map2xp  7277  nnunifi  7358  xpfi  7378  prfi  7381  tpfi  7382  fnfi  7384  pwfi  7402  inf0  7576  cantnffval  7618  cantnfvalf  7620  oemapwe  7650  cantnffval2  7651  cnfcom2  7659  cnfcom3lem  7660  cnfcom3  7661  cnfcom3clem  7662  r1fin  7699  hta  7821  infxpenlem  7895  alephon  7950  alephfplem1  7985  dfac5lem4  8007  dfac5lem5  8008  kmlem10  8039  fin1a2lem10  8289  fin1a2lem12  8291  hsmexlem9  8305  axcc2lem  8316  domtriomlem  8322  axdc2lem  8328  axcclem  8337  brdom7disj  8409  brdom6disj  8410  iundom2g  8415  konigthlem  8443  canthwelem  8525  wunex2  8613  wunex3  8616  nqex  8800  1nq  8805  1pr  8892  axcnex  9022  ax1cn  9024  negex  9304  inelr  9990  cju  9996  nnexALT  10002  2re  10069  3re  10071  4re  10073  5re  10075  6re  10076  7re  10077  8re  10078  9re  10079  10re  10080  2nn  10133  3nn  10134  4nn  10135  5nn  10136  6nn  10137  7nn  10138  8nn  10139  9nn  10140  10nn  10141  nn0ex  10227  zexALT  10300  nneo  10353  zeo  10355  decex  10384  decnncl  10395  deccl  10396  numnncl2  10399  decnncl2  10400  numsucc  10408  numma2c  10415  numadd  10416  numaddc  10417  nummul1c  10418  nummul2c  10419  qexALT  10589  xrex  10609  pnfxr  10713  mnfxr  10714  xnegex  10794  xnegcl  10799  ixxssxr  10928  om2uzuzi  11289  ltweuz  11301  axdc4uzlem  11321  seqex  11325  m1expcl2  11403  faccl  11576  facwordi  11580  faclbnd2  11582  bccl  11613  hashrabrsn  11648  hashunlei  11684  hashpw  11699  s1cli  11757  cats1un  11790  revs1  11797  cats1cli  11821  cats1fvn  11822  crre  11919  remim  11922  climmpt  12365  climle  12433  climsup  12463  sumex  12481  iserabs  12594  isumshft  12619  supcvg  12635  explecnv  12644  geo2lim  12652  ere  12691  eftlub  12710  efsep  12711  tan0  12752  ef01bndlem  12785  divalglem5  12917  divalglem9  12921  sadcf  12965  smupf  12990  crt  13167  phimullem  13168  eulerthlem2  13171  pczpre  13221  pockthi  13275  prmreclem2  13285  igz  13302  0ramcl  13391  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  1259prm  13455  2503lem1  13456  2503lem2  13457  2503lem3  13458  2503prm  13459  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  ndxarg  13489  ressbas  13519  ressbas2  13520  ressid  13524  strle1  13560  topnid  13663  prdsbasex  13674  prdsplusg  13681  prdsmulr  13682  prdsvsca  13683  prdsle  13684  prdsds  13686  prdshom  13689  prdsco  13690  pwselbasb  13710  pwsvscafval  13716  pwssca  13718  pwssnf1o  13720  imassca  13745  imasvsca  13746  imasle  13748  xpslem  13798  xpssca  13803  xpsvsca  13804  isacs2  13878  cidfval  13901  homffval  13917  comfffval  13924  oppchomfval  13940  oppccofval  13942  oppccatid  13945  monfval  13958  oppcmon  13964  sectffval  13976  invffval  13983  isoval  13990  rescbas  14029  reschom  14030  rescco  14032  subccatid  14043  fullsubc  14047  isfunc  14061  isfuncd  14062  idfu2nd  14074  idfu1st  14076  cofu1st  14080  cofu2nd  14082  funcres2c  14098  ressffth  14135  fuccofval  14156  fuchom  14158  fucco  14159  fuccatid  14166  fucid  14168  invfuc  14171  homafval  14184  arwval  14198  idafval  14212  coafval  14219  coapm  14226  setccatid  14239  catchomfval  14253  catccofval  14255  catccatid  14257  xpcbas  14275  xpchomfval  14276  xpccofval  14279  xpccatid  14285  1stf1  14289  1stf2  14290  2ndf1  14292  2ndf2  14293  prf1  14297  prf2fval  14298  evlf2  14315  evlf1  14317  curf1fval  14321  curf11  14323  curf12  14324  curf1cl  14325  curf2  14326  curf2cl  14328  hof2fval  14352  yonedalem4a  14372  yonedalem4c  14374  yonedalem3  14377  yonedainv  14378  isdrs  14391  ispos  14404  isposix  14414  pltfval  14416  lubfval  14435  lubval  14436  lubprop  14437  glbfval  14440  glbval  14441  glbprop  14442  joinfval  14444  joinlem  14447  meetfval  14451  meetlem  14454  clatlem  14539  isglbd  14544  odupos  14562  oduglb  14566  odumeet  14567  odulub  14568  odujoin  14569  ipolt  14585  ipopos  14586  isacs4lem  14594  isdlat  14619  plusffval  14702  issubmnd  14724  ismhm  14740  0mhm  14758  submacs  14765  pwsdiagmhm  14768  gsumvalx  14774  gsumval  14775  gsumress  14777  gsumz  14781  frmdplusg  14799  grpinvfval  14843  grpsubfval  14847  grplactfval  14885  mulgfval  14891  mulgval  14892  issubg  14944  0subg  14965  subgacs  14975  nsgacs  14976  nmznsg  14984  eqgfval  14988  eqgen  14993  isghm  15006  gicen  15064  isga  15068  subgga  15077  orbstafun  15088  orbstaval  15089  orbsta  15090  orbsta2  15091  symgplusg  15099  cayleylem2  15111  cntzfval  15119  cntzval  15120  oppgplusfval  15144  odfval  15171  odval  15172  odinf  15199  dfod2  15200  pgpfi1  15229  pgp0  15230  sylow1lem2  15233  sylow2alem2  15252  sylow2blem1  15254  sylow2blem2  15255  sylow3lem6  15266  lsmfval  15272  lsmvalx  15273  oppglsm  15276  pj1fval  15326  efglem  15348  efgtf  15354  efgsval2  15365  efgsp1  15369  efgrelexlemb  15382  efgcpbllemb  15387  frgpeccl  15393  frgpmhm  15397  vrgpval  15399  frgpuplem  15404  frgpupf  15405  frgpupval  15406  frgpup1  15407  frgpup3lem  15409  frgpnabllem1  15484  frgpnabllem2  15485  iscygodd  15498  prmcyg  15503  lt6abl  15504  dprdfeq0  15580  dmdprdsplitlem  15595  ablfacrplem  15623  ablfacrp  15624  ablfacrp2  15625  ablfac1a  15627  ablfac1b  15628  ablfac1c  15629  ablfac1eu  15631  pgpfaclem2  15640  ablfaclem1  15643  ablfaclem2  15644  ablfaclem3  15645  mgpplusg  15652  mgpress  15659  pwsmgp  15724  opprmulfval  15730  dvdsrval  15750  isunit  15762  unitgrp  15772  unitlinv  15782  unitrinv  15783  dvrfval  15789  isirred  15804  isdrng2  15845  drngmcl  15848  drngid2  15851  issubrg  15868  subrgugrp  15887  isabv  15907  staffval  15935  islmod  15954  scaffval  15968  lssset  16010  islss  16011  lsssn0  16024  lssacs  16043  lspfval  16049  lspval  16051  lspcl  16052  lspuni0  16086  lss0v  16092  0lmhm  16116  lmhmvsca  16121  islbs  16148  islbs3  16227  lbsextlem1  16230  lbsextlem3  16232  lbsextlem4  16233  lbsext  16235  rsp1  16295  drngnidl  16300  2idlval  16304  divsrhm  16308  isnzr2  16334  rrgval  16347  aspval  16387  asclfval  16393  gsumbagdiag  16441  psrbas  16443  psrelbas  16444  psrplusg  16445  psrmulr  16448  psrmulfval  16449  psrmulcllem  16451  psrvscafval  16454  psrvscaval  16456  psrvscacl  16457  psr0cl  16458  psr0lid  16459  psrnegcl  16460  psrlinv  16461  psr1cl  16466  psrlidm  16467  psrridm  16468  psrdi  16470  psrdir  16471  psrass23  16473  resspsradd  16479  resspsrmul  16480  resspsrvsca  16481  mvrval  16485  mvrval2  16486  mplsubglem  16498  mpladd  16505  mplmul  16506  mplvscaval  16511  ressmpladd  16520  ressmplmul  16521  ressmplvsca  16522  subrgmvr  16524  mplmon  16526  mplmonmul  16527  mplcoe1  16528  ltbval  16532  opsrle  16536  opsrtoslem2  16545  mplmon2  16553  psrbag0  16554  psrbagsn  16555  subrgascl  16558  evlslem2  16568  psr1baslem  16583  ressply1add  16624  ressply1mul  16625  ressply1vsca  16626  psropprmul  16632  coe1tmmul2fv  16670  coe1pwmulfv  16672  ply1coe  16684  xrsex  16716  expghm  16777  zrhrhmb  16792  zlmlem  16798  zlmsca  16802  zlmvsca  16803  znle  16817  znbas  16824  znzrhval  16827  zntoslem  16837  znfi  16840  znidomb  16842  znunithash  16845  ipffval  16879  ocvfval  16893  ocvval  16894  elocv  16895  thlbas  16923  thlle  16924  thlleval  16925  thloc  16926  pjfval  16933  pjdm  16934  pjpm  16935  isobs  16947  indistopon  17065  iccordt  17278  concompid  17494  ptbasfi  17613  imastopn  17752  ptcmpfi  17845  uzrest  17929  tmdgsum2  18126  distgp  18129  indistgp  18130  cldsubg  18140  snclseqg  18145  tsmsval  18160  tsmsadd  18176  ustfn  18231  ust0  18249  ustn0  18250  ussid  18290  isusp  18291  ressust  18294  cnextucn  18333  prdsxmetlem  18398  tmslem  18512  nrmmetd  18622  nmfval  18636  tnglem  18681  tngds  18689  tngnm  18692  tngngp2  18693  tngngpd  18694  tngngp  18695  nghmfval  18756  nmo0  18769  cnbl0  18808  remet  18821  re2ndc  18832  xrrest  18838  zcld  18844  icccmp  18856  xrge0gsumle  18864  xrge0tsms  18865  xmetdcn  18869  divcn  18898  expcn  18902  iicon  18917  climcncf  18930  cnmpt2pc  18953  cnrehmeo  18978  cnheiborlem  18979  rellycmp  18982  bndth  18983  evth2  18985  pi1bas  19063  cphsubrglem  19140  cphcjcl  19146  tchex  19176  ipcau2  19191  cncmet  19275  cmsss  19303  ishl2  19324  minveclem4a  19331  minveclem4  19333  finiunmbl  19438  ioombl1lem4  19455  vitalilem4  19503  vitalilem5  19504  ismbf2d  19533  mbfimaopnlem  19547  mbflimsup  19558  mbflim  19560  mbfi1fseqlem6  19612  itgex  19662  bddmulibl  19730  ditgex  19739  recnperf  19792  dv11cn  19885  dvcnvrelem2  19902  ftc1  19926  evlslem3  19935  evlslem1  19936  evlsval2  19941  evl1fval  19947  evl1val  19948  evl1rhm  19949  evl1sca  19950  evl1var  19952  evl1addd  19954  evl1subd  19955  evl1muld  19956  evl1expd  19958  pf1f  19970  pf1mpf  19972  pf1ind  19975  mdegfval  19985  mdegldg  19989  mdegcl  19992  mdegmullem  20001  uc1pval  20062  mon1pval  20064  q1pval  20076  r1pval  20079  ply1remlem  20085  ply1rem  20086  facth1  20087  fta1glem1  20088  fta1glem2  20089  fta1blem  20091  ig1pval  20095  plyeq0lem  20129  quotval  20209  elqaalem3  20238  aaliou3lem4  20263  ulmcau  20311  ulmdvlem1  20316  ulmdvlem3  20318  mbfulm  20322  itgulm  20324  dvradcnv  20337  pserdvlem2  20344  sincn  20360  coscn  20361  tanabsge  20414  reloggim  20493  logcn  20538  dvloglem  20539  logdmopn  20540  dvlog2  20544  cxpcn  20629  cxpcn3  20632  resqrcn  20633  ang180lem3  20653  atanrecl  20751  atan1  20768  atansopn  20772  birthdaylem1  20790  birthday  20793  emcllem4  20837  emcllem6  20839  basellem6  20868  ppiublem1  20986  dchrplusg  21031  dchrmulid2  21036  dchrinvcl  21037  dchrptlem2  21049  dchrsum2  21052  sumdchr2  21054  dchr2sum  21057  bposlem6  21073  bposlem8  21075  lgslem4  21083  lgsdir2lem2  21108  selberglem1  21239  selberglem3  21241  selberg  21242  selbergs  21268  qdrng  21314  usgraexmpl  21420  nbgraf1o0  21456  wlkntrl  21562  0pth  21570  constr1trl  21588  constr2wlk  21598  constr2trl  21599  constr2spth  21600  constr2pth  21601  constr3lem1  21632  constr3trllem3  21639  eupatrl  21690  eupath  21703  konigsberg  21709  gxval  21846  issubgoi  21898  rngoi  21968  dvrunz  22021  isvci  22061  isnvi  22092  imsmetlem  22182  dipfval  22198  sspval  22222  islno  22254  nmooval  22264  nmounbseqi  22278  nmobndseqi  22280  bloval  22282  0ofval  22288  0oval  22289  blocni  22306  ajfval  22310  hmoval  22311  cncph  22320  isph  22323  phpar  22325  ipasslem7  22337  siilem2  22353  ajval  22363  ubthlem1  22372  ubthlem2  22373  minvecolem4b  22380  minvecolem4  22382  minvecolem5  22383  hlex  22400  normlem2  22613  normlem3  22614  normlem6  22617  h0elch  22757  hhsssh  22769  spansnji  23148  nonbooli  23153  3oalem5  23168  3oalem6  23169  3oai  23170  mayetes3i  23232  nmcexi  23529  nmbdfnlb  23553  rnelshi  23562  cnlnadjlem5  23574  pjbdlni  23652  golem2  23775  goeqi  23776  ress0g  24182  ressplusf  24183  ressnm  24184  xrge0tsmsd  24223  rdivmuldivd  24227  rnginvval  24228  dvrcan5  24229  ofldlt1  24243  inftmrel  24250  isinftm  24251  relt  24276  redvr  24277  retos  24278  refld  24279  pstmfval  24291  tpr2tp  24302  tpr2rico  24310  mndpluscn  24312  xrge0pluscn  24326  xrge0mulc1cn  24327  xrge0haus  24330  lmlimxrge0  24334  lmxrge0  24337  qqhval  24358  qqhcn  24375  qqhucn  24376  esumex  24426  esumcst  24455  hasheuni  24475  esumcvg  24476  isrnsigaOLD  24495  prsiga  24514  brsiga  24537  mbfmcnt  24618  sxbrsigalem3  24622  dya2iocuni  24633  dya2iocucvr  24634  sxbrsigalem1  24635  sxbrsiga  24640  sibf0  24649  sibfof  24654  sitgclg  24656  coinflipprob  24737  coinfliprv  24740  lgamgulmlem5  24817  lgamgulmlem6  24818  lgamgulm2  24820  lgamcvglem  24824  subfacp1lem1  24865  subfacp1lem3  24868  subfacp1lem5  24870  subfacp1lem6  24871  kur14lem7  24898  iiscon  24939  iillyscon  24940  cvmliftlem5  24976  cvmliftlem8  24979  cvmliftlem10  24981  cvmlift2lem9  24998  ghomgrpilem2  25097  ghomsn  25099  ghomgrplem  25100  circum  25111  climlec3  25214  prodfclim1  25221  prodex  25233  predasetex  25455  trpredex  25515  altopex  25805  colinearex  25994  bpoly4  26105  rankeq1o  26112  ssoninhaus  26198  areacirc  26297  upixp  26431  sdclem2  26446  sdclem1  26447  fdc  26449  lmclim2  26464  caures  26466  idcncf  26469  cncfres  26474  heibor1lem  26518  heiborlem3  26522  heibor  26530  rrnval  26536  rrnmet  26538  reheibor  26548  grpokerinj  26560  isdrngo1  26572  isdrngo2  26574  isrngohom  26581  idlval  26623  isidl  26624  0idl  26635  0rngo  26637  divrngidl  26638  smprngopr  26662  igenval  26671  mapfzcons2  26775  jm2.23  27067  jm2.27dlem2  27081  jm2.27dlem4  27083  rmydioph  27085  rmxdioph  27087  expdiophlem2  27093  expdioph  27094  aomclem6  27134  islssfgi  27147  pwssplit4  27168  pwslnmlem0  27170  frlmbas  27200  frlmbasf  27205  frlmvscafval  27207  uvcvval  27212  uvcvvcl  27213  frlmsslss2  27222  frlmlbs  27226  ellspd  27231  elfilspd  27232  mapfien2  27235  pwfi2en  27238  frlmpwfi  27239  islinds2  27260  lsslindf  27277  lsslinds  27278  islindf4  27285  hbtlem1  27304  hbtlem7  27306  mncn0  27321  aaitgo  27344  symgfisg  27386  psgnfval  27400  cnmsgnsubg  27411  psgnghm  27414  psgnghm2  27415  mndvcl  27423  mamucl  27433  mamudiagcl  27434  mamulid  27435  mamurid  27436  mamuvs1  27440  mamuvs2  27441  matmulr  27444  mdetfval  27464  mendplusgfval  27470  mendmulrfval  27472  mendvscafval  27475  subrgacs  27485  sdrgacs  27486  cntzsdrg  27487  idomrootle  27488  idomodle  27489  deg1mhm  27503  rfcnpre1  27666  fcnre  27672  refsumcn  27677  refsum2cnlem1  27684  clim1fr1  27703  climexp  27707  climinf  27708  climneg  27712  climdivf  27714  itgsin0pilem1  27720  stoweidlem47  27772  stoweidlem53  27778  stoweidlem57  27782  stoweidlem59  27784  wallispilem3  27792  wallispilem4  27793  wallispilem5  27794  wallispi  27795  stirlinglem1  27799  stirlinglem8  27806  stirlinglem12  27810  stirlinglem13  27811  stirlinglem14  27812  stirlinglem15  27813  cshwsexa  28291  usgra2adedgwlkon  28317  dpval  28513  bnj105  29089  bnj918  29135  bnj95  29235  bnj852  29292  bnj865  29294  lshpset  29776  lsatset  29788  lcvfbr  29818  islfl  29858  lfl0f  29867  lfl1  29868  lfladd0l  29872  lflnegl  29874  lflvscl  29875  lflvsdi1  29876  lflvsdi2  29877  lflvsdi2a  29878  lflvsass  29879  lfl0sc  29880  lflsc0N  29881  lfl1sc  29882  lkrfval  29885  lkr0f  29892  lkrsc  29895  eqlkr2  29898  ldualvbase  29924  ldualfvadd  29926  ldualvaddval  29929  ldualsca  29930  ldualfvs  29934  ldualvsval  29936  isopos  29978  cmtfvalN  30008  cvrfval  30066  pats  30083  glbconN  30174  llnset  30302  lplnset  30326  lvolset  30369  lineset  30535  isline  30536  pointsetN  30538  psubspset  30541  ispsubsp  30542  pmapfval  30553  pmapval  30554  paddfval  30594  paddval  30595  pclfvalN  30686  pclvalN  30687  polfvalN  30701  polvalN  30702  psubclsetN  30733  ispsubclN  30734  watfvalN  30789  watvalN  30790  lhpset  30792  lautset  30879  islaut  30880  pautsetN  30895  ispautN  30896  ldilfset  30905  ldilset  30906  ltrnfset  30914  ltrnset  30915  dilfsetN  30949  dilsetN  30950  trnfsetN  30952  trlfset  30957  cdleme25cl  31154  cdleme26e  31156  cdleme26eALTN  31158  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme29cl  31174  cdleme31snd  31183  cdleme31fv  31187  cdlemefrs29clN  31196  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme41sn3a  31230  cdleme32a  31238  cdleme40m  31264  cdleme40n  31265  cdleme42b  31275  cdlemeg46c  31310  tgrpfset  31541  tgrpbase  31543  tgrpopr  31544  tendofset  31555  istendo  31557  tendopl  31573  tendo02  31584  tendoi  31591  erngfset  31596  erngbase  31598  erngfplus  31599  erngfmul  31602  erngfset-rN  31604  erngbase-rN  31606  erngfplus-rN  31607  erngfmul-rN  31610  cdlemk29-3  31708  cdlemk36  31710  cdlemk40  31714  cdlemkid5  31732  cdlemkid  31733  cdlemk56  31768  dvafset  31801  dvasca  31803  dvavbase  31810  dvafvadd  31811  dvafvsca  31813  diaffval  31828  diafval  31829  diaval  31830  dvhfset  31878  dvhsca  31880  dvhvbase  31885  dvhfvadd  31889  dvhfvsca  31898  docaffvalN  31919  docafvalN  31920  docavalN  31921  djaffvalN  31931  djafvalN  31932  djavalN  31933  dibffval  31938  dibfval  31939  dibopelvalN  31941  dibopelval2  31943  dibelval3  31945  diblsmopel  31969  dicffval  31972  dicfval  31973  dicval  31974  cdlemn11a  32005  dihffval  32028  dihfval  32029  dihvalcqpre  32033  dihopelvalcpre  32046  dihord6apre  32054  dihpN  32134  dochffval  32147  dochfval  32148  dochval  32149  djhffval  32194  djhfval  32195  djhval  32196  islpolN  32281  lpolconN  32285  dochpolN  32288  lcfrlem8  32347  lcfrlem9  32348  lcdfval  32386  lcd0vvalN  32411  mapdffval  32424  mapdfval  32425  mapdval  32426  mapd1o  32446  mapdunirnN  32448  mapdhval  32522  mapdhval0  32523  hvmapffval  32556  hvmapfval  32557  hvmapval  32558  hdmap1ffval  32594  hdmap1fval  32595  hdmap1vallem  32596  hdmapffval  32627  hdmapfval  32628  hgmapffval  32686  hgmapfval  32687  hlhilset  32735  hlhilsca  32736  hlhilbase  32737  hlhilplus  32738  hlhilvsca  32748  hlhilip  32749  hlhilnvl  32751  hlhillsm  32757  hlhillcs  32759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator