Theorem breq2 4441

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq2	|- ( A = B -> ( C R A <-> C R B ) )

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 4203	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2512	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4438	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4438	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 288	1 |- ( A = B -> ( C R A <-> C R B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1383   e. wcel 1804   <.cop 4020   class class class wbr 4437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438

This theorem is referenced by:  breq12  4442  breq2i  4445  breq2d  4449  nbrne1  4454  pocl  4797  swopolem  4799  swopo  4800  solin  4813  sotric  4816  sotrieq  4817  isso2i  4822  somo  4824  seex  4832  frirr  4846  fr2nr  4847  frminex  4849  wereu2  4866  vtoclr  5034  posn  5058  frsn  5060  brcog  5159  brcogw  5161  opelcnvg  5172  dfdmf  5186  breldmg  5198  dfrnf  5231  dmcoss  5252  resieq  5274  dfres2  5316  elimag  5331  elrelimasn  5351  elimasn  5352  asymref2  5374  intirr  5375  poirr2  5381  sotri3  5387  poltletr  5392  soltmin  5396  dffun3  5589  dffun6f  5592  fun11  5643  brprcneu  5849  fv3  5869  tz6.12c  5875  tz6.12i  5876  funbrfv  5896  fnbrfvb  5898  funfv2f  5927  dffv2  5931  fvopab5  5964  fndmdif  5976  dff3  6029  fmptco  6049  foeqcnvco  6188  isorel  6207  soisores  6208  soisoi  6209  isocnv  6211  isotr  6217  isopolem  6226  isosolem  6228  f1oiso  6232  f1oiso2  6233  caovordig  6465  caovordg  6467  caovord  6471  caofrss  6558  caoftrn  6560  fr3nr  6600  dfwe2  6602  f1oweALT  6769  frxp  6895  poxp  6897  suppimacnv  6914  tposoprab  6993  ertr  7328  ecopovsym  7415  ecopovtrn  7416  domeng  7532  eqeng  7551  snfi  7598  sbth  7639  domunsn  7669  domssex  7680  nneneq  7702  php2  7704  onfin  7710  1sdom  7724  unxpdom  7729  isinf  7735  fineqvlem  7736  pssnn  7740  ssnnfi  7741  dif1enOLD  7754  dif1en  7755  findcard  7761  findcard2  7762  findcard3  7765  frfi  7767  fisupg  7770  nnsdomg  7781  unfi  7789  fiint  7799  mapfien2  7870  supmo  7914  eqsup  7918  supub  7921  suplub  7922  suplub2  7923  supmax  7926  supmaxlemOLD  7927  fisup2g  7929  fisupcl  7930  suppr  7932  supisolem  7934  supisoex  7935  ordtypecbv  7945  ordtypelem3  7948  ordtypelem6  7951  ordtypelem7  7952  ordtypelem9  7954  wemaplem1  7974  wemaplem2  7975  harval  7991  wemapwe  8142  wemapweOLD  8143  r111  8196  cardf2  8327  isnum2  8329  cardval3  8336  cardnueq0  8348  carden2a  8350  cardlim  8356  isinffi  8376  onsdom  8380  harval2  8381  cardmin2  8382  ondomen  8421  alephnbtwn  8455  alephinit  8479  aceq3lem  8504  infmap2  8601  cfslb2n  8651  sornom  8660  isfin4  8680  fin23lem26  8708  fin23lem27  8711  fin1a2lem11  8793  fin1a2lem12  8794  hsmex  8815  domtriomlem  8825  dominf  8828  zorn2lem2  8880  zorn2lem7  8885  zorn2g  8886  axdclem  8902  axdc  8904  fodomg  8906  brdom7disj  8912  brdom6disj  8913  cardmin  8942  ficard  8943  alephval2  8950  dominfac  8951  cfpwsdom  8962  gchi  9005  fpwwe2lem12  9022  fpwwe2lem13  9023  canthp1lem1  9033  canthp1lem2  9034  pwfseqlem4a  9042  pwfseqlem4  9043  elina  9068  winainflem  9074  eltskg  9131  rankcf  9158  indpi  9288  nqereu  9310  nsmallnq  9358  ltbtwnnq  9359  ltrnq  9360  prcdnq  9374  genpcd  9387  genpnmax  9388  ltaddpr2  9416  ltexprlem4  9420  prlem936  9428  reclem2pr  9429  reclem3pr  9430  supexpr  9435  ltsosr  9474  ltasr  9480  recexsrlem  9483  mulgt0sr  9485  map2psrpr  9490  supsrlem  9491  axpre-lttri  9545  axpre-lttrn  9546  axpre-ltadd  9547  axpre-mulgt0  9548  axpre-sup  9549  ltletr  9679  letr  9681  ltne  9684  eqle  9690  dedekind  9747  dedekindle  9748  ltordlem  10085  elimgt0  10385  elimge0  10386  squeeze0  10455  fimaxre2  10498  lbreu  10500  lble  10502  sup2  10506  infm3  10509  suprlub  10512  supmul1  10515  supmullem1  10516  supmullem2  10517  supmul  10518  infmrcl  10529  infmrgelb  10530  nn2ge  10568  nnge1  10569  nnsub  10581  nominpos  10782  nnunb  10798  elnnnn0b  10847  nn0sub  10853  nn0ge2m1nn  10868  peano2uz2  10957  peano5uzi  10958  dfuzi  10960  uzind  10961  uzind3  10963  uzindOLD  10964  uzind3OLD  10965  eluz1  11096  uzind4  11150  uzwo  11155  uzwoOLD  11156  nnwof  11159  indstr2  11171  ublbneg  11177  zsupss  11182  uzsupss  11185  uzwo3  11188  zmin  11189  zmax  11190  zbtwnre  11191  rebtwnz  11192  rpnnen1lem1  11219  rpnnen1lem2  11220  rpnnen1lem3  11221  rpnnen1lem4  11222  rpnnen1lem5  11223  reexALT  11225  elrp  11233  mnfltxr  11347  nn0pnfge0  11352  xrltnsym  11354  xrlttri  11356  xrlttr  11357  xrltletr  11371  xrletr  11372  ngtmnft  11379  xrltmin  11394  xrlemin  11396  ifle  11407  z2ge  11408  qbtwnre  11409  qbtwnxr  11410  qextlt  11413  qextle  11414  xltnegi  11426  xmullem2  11468  xmulasslem2  11485  xmulasslem  11488  xlemul1a  11491  xrsupexmnf  11507  xrsupsslem  11509  xrinfmsslem  11510  xrub  11514  supxrpnf  11521  supxrunb1  11522  supxrunb2  11523  ixxval  11548  elixx1  11549  elioo2  11581  iccid  11585  icc0  11588  iccsupr  11628  repos  11632  supicc  11679  supiccub  11680  supicclub  11681  fzval  11685  elfz1  11688  flval  11913  flval2  11932  flval3  11933  dfceil2  11950  uzsup  11972  modid2  12005  fsequb  12067  ssnn0fi  12076  rabssnn0fi  12077  suppssfz  12082  serge0  12143  expge0  12184  expge1  12185  facdiv  12347  facwordi  12349  hashkf  12389  hashnnn0genn0  12398  hashv01gt1  12400  hashneq0  12416  hashdom  12429  hashnn0n0nn  12440  hashss  12456  hashgt12el  12463  hashgt12el2  12464  hashge2el2dif  12503  brfi1uzind  12514  wrdlen1  12561  fstwrdne0  12563  wrdeqswrdlsw  12656  2swrdeqwrdeq  12660  2swrd1eqwrdeq  12661  ccats1swrdeq  12676  ccats1swrdeqrex  12686  swrdccatin12lem3  12697  2swrd2eqwrdeq  12873  shftfib  12887  shftfn  12888  2shfti  12895  sqrlem3  13060  resqrex  13066  cau3lem  13169  caubnd2  13172  caubnd  13173  sqreu  13175  limsuple  13283  limsupval2  13285  rlim2  13301  climi  13315  rlimi  13318  ello12r  13322  ello1mpt  13326  ello1d  13328  lo1bdd2  13329  lo1bddrp  13330  elo12r  13333  o1lo1  13342  rlimclim1  13350  rlimdm  13356  climeu  13360  climmo  13362  2clim  13377  o1co  13391  o1compt  13392  addcn2  13398  mulcn2  13400  reccn2  13401  cn1lem  13402  rlimo1  13421  lo1add  13431  lo1mul  13432  climsup  13474  caucvgrlem  13477  caucvgb  13484  summo  13521  zsum  13522  fsum  13524  o1fsum  13609  climcnds  13645  supcvg  13649  ntrivcvgn0  13689  ntrivcvgmullem  13692  prodmo  13725  zprod  13726  fprod  13730  fprodntriv  13731  rpnnen2lem4  13933  rpnnen  13942  ruclem2  13947  ruclem12  13956  sqrt2irr  13964  dvdsabsb  13985  0dvds  13986  dvdsle  14013  alzdvds  14018  dvdsext  14019  fzo0dvdseq  14021  divalglem10  14042  bitsinv1lem  14073  sadadd3  14093  bitsuz  14106  gcdval  14128  gcdcllem1  14131  gcdcllem2  14132  gcddvds  14135  bezoutlem4  14161  dvdsgcd  14163  dvdssq  14180  isprm  14201  isprm2lem  14206  dvdsprm  14222  coprmdvds2  14226  isprm6  14232  exprmfct  14233  maxprmfct  14236  prmexpb  14240  prmfac1  14241  rpexp  14243  iserodd  14341  pceu  14352  pczpre  14353  pcdiv  14358  pcdvdsb  14374  pcmpt  14393  pcmptdvds  14395  prmpwdvds  14404  unbenlem  14408  infpnlem2  14411  infpn2  14413  prmreclem1  14416  prmreclem2  14417  prmreclem3  14418  prmreclem5  14420  prmreclem6  14421  vdwlem9  14489  vdwlem10  14490  vdwlem13  14493  ramz  14525  imasleval  14920  mreexexlem3d  15025  mreexexlem4d  15026  mreexexd  15027  prslem  15539  drsdirfi  15546  posi  15558  posasymb  15561  pleval2  15574  plttr  15579  pltletr  15580  pospo  15582  lubprop  15595  lublecllem  15597  glbprop  15608  glble  15609  joinlem  15620  joinle  15623  meetval2lem  15631  meetlem  15634  isglbd  15726  lubl  15729  lubun  15732  pospropd  15743  poslubmo  15755  posglbmo  15756  poslubd  15757  tsrlin  15828  tsrlemax  15829  letsr  15836  eqgen  16233  odeq  16553  odmulg  16557  pgpssslw  16613  sylow2alem2  16617  sylow2blem3  16621  efgval2  16721  efgsfo  16736  efgred  16745  efgredeu  16749  efgcpbllemb  16752  gexex  16838  cyggex2  16878  gsummptnn0fz  16993  gsummptnn0fzfv  16995  pgpfaclem1  17111  pgpfaclem2  17112  pgpfaclem3  17113  ablfaclem2  17116  ablfaclem3  17117  lidldvgen  17882  0ringnnzr  17896  psrass1lem  18008  psrmulval  18018  mplmonmul  18105  opsrtoslem2  18128  coe1mul2  18289  coe1tmmul2fv  18298  coe1pwmulfv  18300  gsummoncoe1  18325  zndvds  18566  znleval  18571  islinds  18822  pmatcoe1fsupp  19180  mp2pm2mplem4  19288  fvmptnn04ifa  19329  fvmptnn04ifd  19332  chfacffsupp  19335  chfacfscmul0  19337  chfacfpmmul0  19341  cpmadumatpoly  19362  cayleyhamilton  19369  cayleyhamiltonALT  19370  ordtbaslem  19667  ordtbas2  19670  ordtopn1  19673  mnfnei  19700  ordtt1  19858  ordthauslem  19862  ordthmeolem  20280  trust  20710  ucncn  20766  imasdsf1olem  20854  comet  20994  stdbdxmet  20996  stdbdmet  20997  stdbdmopn  20999  metcnpi  21025  metcnpi2  21026  metcnpi3  21027  ngptgp  21128  nlmvscnlem1  21173  nrginvrcnlem  21177  nmogelb  21201  nmolb  21202  nghmcn  21230  xrsxmet  21292  icccmplem2  21306  icccmplem3  21307  reconnlem2  21310  xrge0tsms  21317  xmetdcn2  21320  metdsf  21330  metdsge  21331  metdscn  21338  metnrmlem1a  21340  addcnlem  21346  cncfi  21376  elcncf1di  21377  iccpnfhmeo  21423  xrhmeo  21424  cnllycmp  21434  evth  21437  ipcnlem1  21663  lmmcvg  21678  cfili  21685  cncmet  21739  minveclem1  21817  minveclem3b  21821  minveclem6  21827  pmltpclem1  21838  pmltpc  21840  ivthlem2  21842  ivthlem3  21843  cniccbdd  21851  ovolmge0  21866  ovolgelb  21869  ovolctb  21879  ovolunlem1  21886  ovoliunlem1  21891  ovoliun  21894  ovoliun2  21895  ovolshftlem1  21898  ovolscalem1  21902  ovolicc2lem3  21908  ovolicc2lem5  21910  ovolicc2  21911  voliunlem3  21940  ioombl1lem1  21946  ioombl1lem4  21949  uniioombllem2  21970  uniioombllem6  21975  volcn  21993  ismbfd  22025  mbfsup  22049  mbfinf  22050  mbflimsup  22051  itg1ge0  22071  itg1climres  22099  mbfi1fseqlem5  22104  itg2val  22113  itg2const  22125  itg2const2  22126  itg2seq  22127  itg2monolem1  22135  itg2i1fseq  22140  itg2i1fseq2  22141  itg2addlem  22143  itg2cnlem1  22146  itg2cnlem2  22147  itg2cn  22148  isibl  22150  ditgeq2  22231  dveflem  22358  dvferm1lem  22363  rolle  22369  c1lip1  22376  lhop1  22393  dvfsumlem2  22406  dvfsumlem4  22408  dvfsumrlim  22410  dvfsum2  22413  mdegmullem  22456  deg1leb  22473  deg1lt  22476  dvdsq1p  22539  plyeq0lem  22585  dgrco  22650  plydivex  22671  quotcan  22683  aannenlem1  22702  aannenlem2  22703  ulmi  22759  ulmcaulem  22767  ulmcau  22768  ulmbdd  22771  ulmdvlem3  22775  mtestbdd  22778  iblulm  22780  psercnlem1  22798  psercn  22799  abelthlem8  22812  sinhalfpilem  22834  logltb  22962  cxple2  23056  cxpcn3lem  23099  isosctrlem1  23130  leibpilem2  23250  cxploglim  23285  scvxcvx  23293  emcllem6  23308  ftalem3  23326  vmaval  23365  isppw2  23367  muval  23384  fsumdvdscom  23439  dvdsflf1o  23441  dvdsflsumcom  23442  musum  23445  muinv  23447  ppiublem1  23455  chtub  23465  logfac2  23470  bpos1lem  23535  bposlem9  23545  lgsdir  23583  lgsne0  23586  lgsqr  23599  lgsquadlem1  23607  lgsquadlem2  23608  lgsquadlem3  23609  2sqlem6  23622  2sqlem8  23625  2sqlem10  23627  dchrisumlema  23651  dchrisumlem2  23653  dchrisumlem3  23654  dchrvmasumiflem1  23664  dchrisum0fval  23668  dchrisum0ff  23670  dchrisum0flblem2  23672  logsqvma2  23706  pntrsumbnd2  23730  pntrlog2bndlem1  23740  pntpbnd1  23749  pntpbnd2  23750  pntibndlem2  23754  pntibndlem3  23755  pntibnd  23756  pntlemi  23767  pntlem3  23772  pntlemp  23773  pntleml  23774  pnt3  23775  tgldimor  23871  lnopp2hpgb  24110  axcontlem10  24254  uhgra0v  24288  usgra0v  24349  usgra1v  24368  cusgraexg  24447  sizeusglecusg  24464  usgramaxsize  24465  3v3e3cycl1  24622  4cycl4v4e  24644  4cycl4dv  24645  wwlknred  24701  wwlkextwrd  24706  wwlkextfun  24707  wwlkextinj  24708  wwlkextproplem2  24720  wwlkextproplem3  24721  clwlkisclwwlklem1  24765  clwwlkf1  24774  clwwlkext2edg  24780  wwlkext2clwwlk  24781  wwlksubclwwlk  24782  clwlkfclwwlk  24822  clwlkfoclwwlk  24823  rusgranumwlks  24934  isfrgra  24968  vdgfrgragt2  25005  frgrawopreglem2  25023  clwwlkextfrlem1  25054  numclwwlkovf2ex  25064  friendshipgt3  25099  gxval  25238  vacn  25582  nmcvcn  25583  smcnlem  25585  nmobndi  25668  blocni  25698  ubthlem1  25764  ubthlem2  25765  ubthlem3  25766  minvecolem1  25768  minvecolem5  25775  minvecolem6  25776  htthlem  25812  norm3lemt  26047  hcaucvg  26081  hlimconvi  26086  hlim2  26087  chlimi  26130  hlimreui  26135  occl  26200  cmbr3  26504  cmcm  26510  cmcm3  26511  lecm  26513  cnopc  26810  cnfnc  26827  0cnop  26876  0cnfn  26877  idcnop  26878  nmopun  26911  nmcexi  26923  lnconi  26930  branmfn  27002  opsqrlem1  27037  pjnmopi  27045  pjnormssi  27065  stge1i  27135  strlem5  27152  hstrlem5  27160  mddmd2  27206  csmdsymi  27231  cvmd  27233  ela  27236  cvbr4i  27264  chirredlem3  27289  chirredlem4  27290  chirred  27292  atmd  27296  mdsym  27309  mddmdin0i  27328  cdj1i  27330  cdj3i  27338  fmptcof2  27480  isoun  27498  xrge0infss  27558  ishashinf  27584  tleile  27627  toslublem  27633  tosglblem  27635  omndadd  27674  sgnsval  27696  xrnarchi  27706  archirng  27710  archiexdiv  27712  archiabllem1a  27713  archiabllem2a  27716  archiabl  27720  xrge0tsmsd  27753  orngmul  27771  isarchiofld  27785  crefi  27828  pcmplfin  27841  ordtconlem1  27884  rge0scvg  27909  qqhcn  27950  qqhucn  27951  esumcst  28049  esumpinfval  28057  esumpcvgval  28062  esumcvg  28070  oddpwdc  28271  eulerpartlems  28277  eulerpartlemf  28287  eulerpartlemt  28288  eulerpartlemr  28291  eulerpartlemgvv  28293  eulerpartlemn  28298  dstfrvunirn  28391  ballotlemfcc  28410  sgnmulsgp  28467  signslema  28497  lgamgulmlem4  28552  lgamgulmlem5  28553  lgambdd  28557  subfacp1lem1  28601  relexpindlem  29040  relexpind  29041  rtrclreclem.trans  29047  dfpo2  29160  fundmpss  29172  funbreq  29177  dfpred3g  29231  predbrg  29242  poseq  29309  wzel  29356  wsuclem  29357  wsuclb  29360  nodenselem4  29420  nodenselem5  29421  nodense  29425  nocvxminlem  29426  nobndup  29436  nofulllem5  29442  brtxp  29506  brtxp2  29507  brpprod3a  29512  elfix  29529  sscoid  29539  elfuns  29541  fnsingle  29545  brimageg  29553  fnimage  29555  brdomaing  29561  brrangeg  29562  funpartlem  29568  fvtransport  29658  fin2so  30016  supaddc  30017  supadd  30018  heicant  30025  mblfinlem1  30027  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  itg2addnclem  30042  itg2addnc  30045  itg2gt0cn  30046  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  trer  30110  elicc3  30111  finminlem  30112  nn0prpwlem  30116  nn0prpw  30117  fnessref  30151  refssfne  30152  fnemeet2  30161  filnetlem3  30174  frinfm  30202  fdc1  30215  nninfnub  30220  equivbnd  30262  heibor1lem  30281  heiborlem8  30290  iccbnd  30312  lzenom  30679  fphpdo  30727  rencldnfilem  30730  irrapxlem5  30738  irrapxlem6  30739  pellexlem3  30743  pellqrex  30791  pellfundre  30793  pellfundge  30794  pellfundlb  30796  pellfundglb  30797  monotoddzz  30855  oddcomabszz  30856  zindbi  30858  jm2.22  30913  jm2.23  30914  rpnnen3  30950  ttac  30954  fnwe2lem2  30973  aomclem8  30983  hbtlem1  31048  hbtlem5  31053  lcmcllem  31178  dvdslcm  31180  lcmledvds  31181  lcmgcdlem  31188  lcmdvds  31190  nzss  31198  ubelsupr  31349  climinf  31566  mullimc  31576  limcdm0  31578  mullimcf  31583  constlimc  31584  idlimc  31586  limsupre  31601  limcleqr  31604  addlimc  31608  0ellimcdiv  31609  limclner  31611  dvdivbd  31674  dvbdfbdioo  31681  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnxpaek  31693  stoweidlem14  31750  stoweidlem29  31765  stoweidlem31  31767  stoweidlem34  31770  stoweidlem49  31785  wallispilem3  31803  stirlinglem13  31822  stirlinglem14  31823  fourierdlem16  31859  fourierdlem20  31863  fourierdlem21  31864  fourierdlem22  31865  fourierdlem25  31868  fourierdlem39  31882  fourierdlem41  31884  fourierdlem42  31885  fourierdlem51  31894  fourierdlem54  31897  fourierdlem64  31907  fourierdlem77  31920  fourierdlem83  31926  fourierdlem87  31930  fourierdlem103  31946  fourierdlem104  31947  fourierdlem112  31955  fouriersw  31968  etransclem48  32019  rlimdmafv  32216  assintopval  32482  ply1mulgsumlem2  32857  ldepsnlinc  32979  bnj1185  33720  bnj602  33841  bnj1228  33935  bj-seex  34374  oposlem  34782  lub0N  34789  glb0N  34793  omllaw  34843  cvrval  34869  cvrnbtwn  34871  cvrnbtwn2  34875  cvrnbtwn3  34876  cvrcon3b  34877  cvrnbtwn4  34879  cvrcmp  34883  isat  34886  atnlt  34913  atlex  34916  cvlexch1  34928  cvlexchb1  34930  cvlatexch1  34936  glbconN  34976  2llnne2N  35007  cvratlem  35020  cvrat4  35042  ps-1  35076  3at  35089  islln  35105  llncmp  35121  llnnlt  35122  islpln  35129  islpln5  35134  lvolex3N  35137  lplncmp  35161  lplnexllnN  35163  lplnnlt  35164  islvol  35172  lvoli3  35176  islvol5  35178  lvolcmp  35216  lvolnltN  35217  dalem-cly  35270  dalem44  35315  pmapval  35356  pmapglbx  35368  lncvrelatN  35380  lncmp  35382  cdlemblem  35392  llnexchb2  35468  lautle  35683  lautcvr  35691  ldilset  35708  ltrnset  35717  trlset  35761  cdlemc4  35794  cdleme11dN  35862  cdleme20k  35920  cdleme21ct  35930  cdleme22b  35942  tendoex  36576  diafval  36633  diaval  36634  dicfval  36777  dihfval  36833  dihglblem2N  36896  frege70  37765