Theorem eqbrtrd 5133

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 5119	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 260	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  eqbrtrrd  5135  somin2  6135  en1b  9018  domunsncan  9061  fodomfi  9268  infsupprpr  9462  hartogslem1  9500  wemaplem2  9505  infdifsn  9622  ttrclselem2  9691  carddomi2  9952  djuinf  10168  carden  10530  alephsuc3  10560  fpwwe2lem5  10615  fpwwe2lem6  10616  inar1  10755  rankcf  10757  lesub3d  11827  lbinfle  12165  supadd  12178  supmul  12182  rpnnen1lem3  12998  divge1  13081  xrmin1  13198  xrmin2  13199  ifle  13218  qbtwnxr  13221  xltnegi  13237  xleadd1a  13274  xlt2add  13281  xlemul1a  13309  xov1plusxeqvd  13520  elfzo0suble  13731  ubmelm1fzo  13788  flflp1  13836  ceim1l  13876  ceilm1lt  13877  ceille  13879  quoremz  13884  quoremnn0ALT  13886  modlt  13909  modeqmodmin  13973  addmodlteq  13978  seqf1olem1  14073  bernneq  14261  discr  14272  faclbnd2  14323  faclbnd4lem3  14327  hashun2  14415  hashfun  14470  hashf1dmcdm  14477  ccatsymb  14616  ccatrn  14623  sgnsub  15139  01sqrexlem6  15294  01sqrexlem7  15295  rddif  15388  amgm2  15417  icodiamlt  15485  climconst  15590  rlimconst  15591  serclim0  15624  rlimcn1  15635  mulcn2  15643  reccn2  15644  o1mul  15662  o1rlimmul  15666  iserex  15704  climlec2  15706  iserge0  15708  climcau  15718  caucvgrlem  15720  caucvgr  15723  iseraltlem2  15730  iseraltlem3  15731  iseralt  15732  fsumabs  15849  o1fsum  15861  iserabs  15863  climfsum  15868  isumless  15895  climcndslem2  15900  divrcnv  15902  flo1  15904  supcvg  15906  georeclim  15922  geomulcvg  15926  cvgrat  15933  mertenslem1  15934  prodfclim1  15943  fprodle  16046  efcvgfsum  16135  eftlub  16160  eflegeo  16172  tanhlt1  16211  tanhbnd  16212  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  cos01gt0  16242  ruclem2  16283  ruclem3  16284  ruclem9  16289  ruclem11  16291  ruclem12  16292  bitsfzolem  16487  bitsfzo  16488  bitsinv1lem  16494  sadcaddlem  16510  mulgcd  16601  eucalglt  16638  lcmledvds  16652  lcmfledvds  16685  mulgcddvds  16708  coprmproddvdslem  16715  prmind2  16738  isprm5  16761  divdenle  16803  nonsq  16813  pythagtriplem4  16874  pclem  16893  pcpremul  16898  pczdvds  16918  pcprmpw2  16937  qexpz  16956  prmreclem4  16974  prmreclem5  16975  4sqlem10  17002  ramtub  17067  ramub2  17069  prmodvdslcmf  17102  prmgaplem8  17113  natpropd  18031  catciso  18163  p0le  18478  acsdomd  18608  chnind  18672  chnub  18673  chnccat  18677  chnpolleha  18683  triv1nsgd  19234  qusgrp  19252  f1otrspeq  19512  pmtrfrn  19523  pmtrfconj  19531  symggen  19535  psgnunilem4  19562  oddvds2  19631  odcau  19669  pgpfi  19670  pgpssslw  19679  sylow3lem4  19695  efgred2  19818  frgp0  19825  odadd2  19914  oddvdssubg  19920  ablfac1c  20138  ablfac1eu  20140  pgpfaclem3  20150  2nsgsimpgd  20169  isabvd  20915  abvsubtri  20930  cyggic  21722  mplsubrg  22154  psdmplcl  22325  psdmul  22329  coe1sfi  22373  mp2pm2mplem5  22967  en2top  23142  1stcrest  23610  2ndcrest  23611  hausmapdom  23657  ufilen  24087  xmetrtri2  24513  prdsxmetlem  24525  bl2in  24557  xblcntrps  24567  xblcntr  24568  ssblps  24579  ssbl  24580  blssps  24581  blss  24582  blcld  24662  methaus  24677  metustexhalf  24713  nmtri2  24784  tngngp3  24813  nrginvrcnlem  24848  nrginvrcn  24849  nmoi  24885  nmo0  24892  nmoid  24899  blcvx  24955  reperflem  24976  reconnlem2  24985  metdcnlem  24994  metdscn  25014  metnrmlem3  25019  mulc1cncf  25064  iccpnfhmeo  25104  cnheiborlem  25113  cnheibor  25114  lebnumii  25125  pcopt  25181  pcopt2  25182  pcoass  25183  nmoleub2lem  25273  nmoleub2lem3  25274  nmoleub2lem2  25275  ipcau2  25393  tcphcphlem1  25394  nglmle  25461  trirn  25559  rrxdstprj1  25568  minveclem3  25588  ivthlem2  25611  ivthlem3  25612  ivth2  25614  ovollb  25638  ovolsslem  25643  ovollb2lem  25647  ovolctb  25649  ovoliunlem1  25661  ovolsca  25674  ovolicc1  25675  ovolicc2lem4  25679  nulmbl  25694  ioombl1lem4  25720  uniioovol  25738  uniioombllem3a  25743  uniioombllem4  25745  opnmbllem  25760  volcn  25765  volivth  25766  i1fadd  25854  i1fmul  25855  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  mbfi1fseqlem6  25879  itg2const2  25900  itg2seq  25901  itg2uba  25902  itg2split  25908  itg2monolem1  25909  itg2monolem3  25911  itg2i1fseq2  25915  itg2addlem  25917  itg2gt0  25919  itg2cnlem1  25920  itg2cnlem2  25921  itgless  25976  ibladdlem  25979  bddmulibl  25998  dveflem  26138  dvferm1lem  26143  dvferm2lem  26145  dvlip  26152  dvlipcn  26153  dvlip2  26154  dvle  26166  dvivthlem1  26167  lhop1lem  26172  dvcvx  26179  dvfsumabs  26182  dvfsumlem2  26186  dvfsumlem4  26188  dvfsumrlim2  26191  dvfsum2  26193  ftc1a  26196  ftc1lem4  26198  ftc1lem5  26199  deg1sub  26265  ply1divex  26294  deg1submon1p  26310  r1pdeglt  26317  dvdsq1p  26320  fta1glem2  26326  fta1g  26327  plyeq0lem  26367  dgrlt  26423  fta1lem  26468  aalioulem2  26496  aalioulem3  26497  aalioulem4  26498  aaliou3lem2  26506  aaliou3lem9  26513  taylply2  26531  ulmbdd  26561  ulmdvlem1  26563  mtest  26567  mtestbdd  26568  radcnvlem1  26576  radcnvle  26583  pserulm  26585  psercn  26589  pserdvlem2  26591  abelthlem2  26595  abelthlem5  26598  abelthlem7  26601  abelthlem8  26602  abelthlem9  26603  reeff1olem  26609  tangtx  26670  tanord  26703  efif1olem4  26710  logrnaddcl  26739  logcj  26771  logimul  26779  logneg2  26780  logdivlti  26785  divlogrlim  26800  logcnlem3  26809  logcnlem4  26810  efopn  26823  logtayllem  26824  logtayl  26825  cxpcn3lem  26912  cxpaddle  26917  abscxpbnd  26918  asinlem3  27036  asinneg  27051  asinsin  27057  atanlogaddlem  27078  atantan  27088  bndatandm  27094  atans2  27096  atantayl  27102  atantayl2  27103  atantayl3  27104  leibpi  27107  birthdaylem3  27118  rlimcnp  27130  efrlim  27134  cxplim  27136  cxp2lim  27141  cxploglim2  27143  divsqrtsumo1  27148  jensenlem2  27152  amgm  27155  logdifbnd  27158  harmonicbnd4  27175  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgambdd  27201  lgamcvg2  27219  ftalem1  27237  ftalem5  27241  basellem1  27245  basellem8  27252  ppip1le  27325  ppiltx  27341  sqff1o  27346  chtublem  27375  chpub  27384  logfaclbnd  27386  logfacrlim  27388  logexprlim  27389  mersenne  27391  bcmono  27441  bcmax  27442  bposlem2  27449  bposlem5  27452  lgslem3  27463  gausslemma2dlem1a  27529  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1c  27557  2sqblem  27595  chebbnd1  27636  chtppilimlem1  27637  chto1ub  27640  chpchtlim  27643  chpo1ubb  27645  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrisum0flblem1  27672  dchrisum0fno1  27675  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  rplogsum  27691  mudivsum  27694  mulogsumlem  27695  mulog2sumlem1  27698  mulog2sumlem2  27699  vmalogdivsum2  27702  2vmadivsumlem  27704  selberglem2  27710  selberg2b  27716  logdivbnd  27720  selberg3lem1  27721  selberg3lem2  27722  selberg4lem1  27724  pntrmax  27728  pntrsumo1  27729  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem2  27755  pntlemb  27761  pntlemg  27762  pntlemh  27763  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemo  27771  pnt  27778  padicabv  27794  ostth2lem2  27798  ostth2lem3  27799  ostth3  27802  nosep1o  27845  nodense  27856  noinfbnd2lem1  27894  noetainflem3  27903  mins1  27935  mins2  27936  eqcuts3  27997  cofcutr  28117  cofcutrtime  28120  addsuniflem  28194  negsunif  28248  sltmuls1  28340  mulsuniflem  28342  precsexlem11  28410  halfcut  28651  pw2cut  28653  bdayfinbndlem1  28660  recut  28687  elreno2  28688  readdscl  28692  remulscllem2  28694  colperpexlem3  29013  mideulem2  29015  lnperpex  29113  trgcopy  29115  iscgra1  29121  prlngplngtr  29209  prlngmid2  29211  prlngsymquadlem  29213  brbtwn2  29255  colinearalglem4  29259  subupgr  29637  crctcshwlkn0lem1  30159  nvabs  31024  nvge0  31025  smcnlem  31049  nmblolbii  31151  blocnilem  31156  siii  31205  ubthlem2  31223  minvecolem3  31228  htthlem  31269  bcsiALT  31531  bcs3  31535  chscllem4  31992  0cnop  32331  0cnfn  32332  nmbdoplbi  32376  nmcoplbi  32380  nmophmi  32383  nmbdfnlbi  32401  nmcfnlbi  32404  nlelchi  32413  riesz1  32417  cnlnadjlem2  32420  nmopadjlei  32440  nmoptrii  32446  nmopcoi  32447  nmopcoadji  32453  unierri  32456  branmfn  32457  pjs14i  32562  hstle  32582  cdj3lem2b  32789  xlt2addrd  33104  eliccelico  33122  elicoelioo  33123  ltesubnnd  33167  2exple2exp  33178  oexpled  33180  wrdt2ind  33273  archirngz  33509  archiabllem2c  33515  dflring3  33787  dflring4  33788  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  ply1degltel  33884  ply1degleel  33885  ig1pmindeg  33892  q1pdir  33893  selvply1rhmlema  33908  extvfvcl  33926  mplvrpmfgalem  33934  esplympl  33957  esplyind  33965  vietadeg1  33968  lbslelsp  33988  ply1degltdimlem  34012  fldextrspunlem1  34065  fldextrspundgle  34068  minplymindeg  34098  minplyirredlem  34100  irredminply  34106  algextdeglem6  34112  rtelextdg2lem  34116  cos9thpiminplylem1  34172  madjusmdetlem2  34218  locfinref  34231  sqsscirc1  34298  tpr2rico  34302  esumcst  34453  esumgect  34480  esum2d  34483  measunl  34606  measiun  34608  omssubaddlem  34689  omssubadd  34690  carsgsigalem  34705  carsgclctunlem2  34709  pmeasmono  34714  eulerpartlemgc  34752  eulerpartlemb  34758  ballotlemsel1i  34903  ballotlemro  34913  signsplypnf  34937  signsply0  34938  signsvtn  34971  signsvfnn  34973  hgt750lemd  35035  logdivsqrle  35037  erdsze2lem1  35695  sinccvglem  36164  divcnvlin  36225  iprodefisum  36233  faclimlem2  36236  fnemeet1  36897  weiunpo  36996  dnibndlem10  37096  dnibndlem11  37097  dnibnd  37100  knoppcnlem4  37105  knoppcnlem6  37107  unblimceq0lem  37115  unbdqndv2lem1  37118  unbdqndv2lem2  37119  knoppndvlem11  37131  knoppndvlem12  37132  knoppndvlem14  37134  knoppndvlem15  37135  knoppndvlem17  37137  knoppndvlem18  37138  knoppndvlem19  37139  knoppndvlem21  37141  ctbssinf  38072  ltflcei  38279  ptrecube  38291  poimirlem16  38307  poimirlem17  38308  poimirlem29  38320  broucube  38325  opnmbllem0  38327  mblfinlem2  38329  mblfinlem3  38330  ismblfin  38332  itg2addnclem  38342  itg2addnclem2  38343  itg2addnclem3  38344  itg2addnc  38345  ibladdnclem  38347  ftc1cnnclem  38362  ftc1cnnc  38363  ftc1anc  38372  geomcau  38430  prdsbnd  38464  cntotbnd  38467  heiborlem4  38485  rrndstprj2  38502  rrncmslem  38503  rrnequiv  38506  iccbnd  38511  cvlcvr1  40133  cvrat3  40236  dalem25  40492  cdlema1N  40585  dalawlem3  40667  dalawlem4  40668  dalawlem5  40669  dalawlem6  40670  dalawlem7  40671  dalawlem9  40673  dalawlem11  40675  dalawlem12  40676  lhp2lt  40795  lhpmcvr  40817  4atexlemcnd  40866  lautj  40887  trlle  40978  trlval3  40981  trlval4  40982  cdleme0moN  41019  cdleme13  41066  cdleme15  41072  cdleme19b  41098  cdleme20e  41107  cdleme20j  41112  cdleme22e  41138  cdleme22eALTN  41139  cdleme26fALTN  41156  cdleme26f  41157  cdleme27N  41163  cdleme41sn3a  41227  cdleme46fsvlpq  41299  cdlemeg46vrg  41321  cdlemg4  41411  cdlemg7N  41420  cdlemg9a  41426  cdlemg11b  41436  cdlemg12a  41437  trljco  41534  tendoidcl  41563  tendococl  41566  tendopltp  41574  tendo0tp  41583  tendoicl  41590  cdlemi2  41613  cdlemk5a  41629  cdlemk5  41630  cdlemk12  41644  cdlemkole  41647  cdlemk14  41648  cdlemk12u  41666  cdlemk37  41708  cdlemk39s-id  41734  cdlemk49  41745  cdlemk39u1  41761  cdlemk39u  41762  dian0  41833  cdlemm10N  41912  cdlemn2  41989  cdlemn10  42000  dihord1  42012  dihord10  42017  dihmeetlem4preN  42100  dihmeetlem18N  42118  dihmeetlem20N  42120  dihjatc  42211  mapdcnvatN  42460  lcmineqlem17  42832  3lexlogpow5ineq2  42842  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  aks4d1p1p3  42856  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p1  42863  aks4d1p3  42865  aks4d1p5  42867  aks4d1p6  42868  aks4d1p7d1  42869  aks4d1p7  42870  aks4d1p8  42874  isprimroot2  42881  posbezout  42887  primrootspoweq0  42893  aks6d1c1p8  42902  aks6d1c1  42903  hashscontpow1  42908  aks6d1c2lem4  42914  aks6d1c2  42917  aks6d1c5lem1  42923  aks6d1c5lem3  42924  2ap1caineq  42932  sticksstones7  42939  sticksstones10  42942  sticksstones11  42943  sticksstones12a  42944  sticksstones12  42945  sticksstones22  42955  aks6d1c6lem2  42958  aks6d1c6lem3  42959  aks6d1c6lem4  42960  aks6d1c6lem5  42964  bcled  42965  bcle2d  42966  aks6d1c7lem1  42967  aks6d1c7lem2  42968  aks5lem3a  42976  unitscyglem1  42982  unitscyglem4  42985  unitscyglem5  42986  aks5  42991  sn-reclt0d  43275  evlselv  43341  fltltc  43413  lzenom  43521  irrapxlem2  43570  irrapxlem3  43571  irrapxlem5  43573  pellexlem2  43577  pell14qrgt0  43606  pellfundlb  43631  pellfundex  43633  pellfund14  43645  rmspecsqrtnq  43653  jm2.24nn  43706  jm2.17a  43707  jm2.17b  43708  congabseq  43721  acongrep  43727  acongeq  43730  jm2.26lem3  43748  jm2.27a  43752  jm2.27c  43754  hbtlem2  43871  dgraaub  43895  idomodle  43938  safesnsupfidom1o  44163  sqrtcval  44387  relexpxpmin  44463  frege102d  44500  hashnzfzclim  45052  binomcxplemfrat  45081  binomcxplemnotnn0  45086  suprnmpt  45912  mpct  45938  rnmptbddlem  45979  dstregt0  46021  lefldiveq  46031  fzisoeu  46039  upbdrech  46044  ssfiunibd  46048  fzdifsuc2  46049  xadd0ge  46058  supxrgere  46069  supxrge  46074  suplesup  46075  xrlexaddrp  46088  infxrunb2  46103  infleinflem2  46106  reclt0d  46122  infrpgernmpt  46199  rexanuz2nf  46226  ioondisj2  46229  iccshift  46254  iooshift  46258  fmul01  46316  fmul01lt1lem1  46320  fmul01lt1lem2  46321  climrec  46339  climsuse  46344  mullimc  46352  mullimcf  46359  constlimc  46360  idlimc  46362  divcnvg  46363  limcperiod  46364  limcrecl  46365  lptioo2  46367  lptioo1  46368  islpcn  46373  lptre2pt  46374  limcleqr  46378  neglimc  46381  addlimc  46382  0ellimcdiv  46383  limclner  46385  climleltrp  46410  limsuplesup  46433  limsupmnflem  46454  supcnvlimsupmpt  46475  0cnv  46476  xlimconst  46559  xlimliminflimsup  46596  sinaover2ne0  46602  cncfshift  46608  cncfperiod  46613  cncfioobdlem  46630  cncfioobd  46631  fperdvper  46653  dvdivbd  46657  dvbdfbdioolem1  46662  dvbdfbdioolem2  46663  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnmul  46677  dvnprodlem1  46680  itgiccshift  46714  itgperiod  46715  ismbl3  46720  ovolsplit  46722  stoweidlem1  46735  stoweidlem11  46745  stoweidlem13  46747  stoweidlem14  46748  stoweidlem16  46750  stoweidlem21  46755  stoweidlem25  46759  stoweidlem26  46760  stoweidlem36  46770  stoweidlem38  46772  stoweidlem41  46775  stoweidlem42  46776  stoweidlem45  46779  stoweidlem48  46782  stoweidlem52  46786  stoweidlem62  46796  wallispilem3  46801  stirlinglem5  46812  stirlinglem6  46813  stirlinglem7  46814  stirlinglem10  46817  stirlinglem12  46819  stirlinglem15  46822  dirkercncflem1  46837  fourierdlem10  46851  fourierdlem12  46853  fourierdlem15  46856  fourierdlem16  46857  fourierdlem19  46860  fourierdlem20  46861  fourierdlem21  46862  fourierdlem22  46863  fourierdlem24  46865  fourierdlem30  46871  fourierdlem37  46878  fourierdlem39  46880  fourierdlem40  46881  fourierdlem41  46882  fourierdlem42  46883  fourierdlem47  46887  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem52  46892  fourierdlem54  46894  fourierdlem60  46900  fourierdlem61  46901  fourierdlem63  46903  fourierdlem64  46904  fourierdlem68  46908  fourierdlem71  46911  fourierdlem72  46912  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem76  46916  fourierdlem77  46917  fourierdlem78  46918  fourierdlem79  46919  fourierdlem81  46921  fourierdlem82  46922  fourierdlem83  46923  fourierdlem84  46924  fourierdlem87  46927  fourierdlem92  46932  fourierdlem93  46933  fourierdlem94  46934  fourierdlem101  46941  fourierdlem102  46942  fourierdlem103  46943  fourierdlem104  46944  fourierdlem111  46951  fourierdlem112  46952  fourierdlem113  46953  fourierdlem114  46954  sqwvfoura  46962  sqwvfourb  46963  fouriersw  46965  elaa2lem  46967  etransclem23  46991  etransclem28  46996  etransclem32  47000  etransclem35  47003  etransclem48  47016  qndenserrnbllem  47028  rrnprjdstle  47035  ioorrnopnlem  47038  ioorrnopnxrlem  47040  salexct  47068  sge0fsum  47121  sge0supre  47123  sge0rnbnd  47127  sge0lefi  47132  sge0lessmpt  47133  sge0ltfirp  47134  sge0prle  47135  sge0resrnlem  47137  sge0le  47141  sge0split  47143  sge0iunmptlemre  47149  sge0iunmpt  47152  sge0isum  47161  sge0xaddlem1  47167  sge0xaddlem2  47168  sge0xadd  47169  sge0reuz  47181  sge0reuzb  47182  meaunle  47198  meaiunlelem  47202  voliunsge0lem  47206  meaiuninc  47215  meaiininclem  47220  omeunle  47250  omeiunle  47251  omelesplit  47252  omeiunltfirp  47253  carageniuncllem2  47256  caratheodorylem2  47261  caragencmpl  47269  ovnlecvr  47292  ovncvrrp  47298  ovnsubaddlem1  47304  ovnsubadd  47306  hoidmv1lelem1  47325  hoidmv1lelem2  47326  hoidmv1le  47328  hoidmvlelem1  47329  hoidmvlelem2  47330  hoidmvlelem5  47333  hoidmvle  47334  ovnhoilem1  47335  ovnlecvr2  47344  ovncvr2  47345  hoiqssbllem2  47357  hspmbllem2  47361  hspmbllem3  47362  ovnsplit  47382  ovolval5lem1  47386  vonioolem1  47414  vonioolem2  47415  vonicclem1  47417  vonicclem2  47418  pimconstlt1  47436  smflimlem2  47506  smflimlem4  47508  smfmullem1  47525  smfsuplem1  47545  smflimsuplem4  47557  smflimsuplem5  47558  chnerlem1  47618  chner  47621  difmodm1lt  48122  2timesltsqm1  48136  iccpartltu  48194  iccpartleu  48197  pgrple2abl  49165  nnpw2blen  49380  dignn0flhalflem1  49415  2itscp  49581  functermclem  50305