Theorem eqbrtrd 5122

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 5110	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 259	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1560   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  eqbrtrrd  5124  somin2  6122  en1b  9006  domunsncan  9049  fodomfi  9256  infsupprpr  9452  hartogslem1  9490  wemaplem2  9495  infdifsn  9612  ttrclselem2  9681  carddomi2  9928  djuinf  10145  carden  10508  alephsuc3  10538  fpwwe2lem5  10593  fpwwe2lem6  10594  inar1  10733  rankcf  10735  lesub3d  11805  lbinfle  12147  supadd  12160  supmul  12164  rpnnen1lem3  12980  divge1  13063  xrmin1  13180  xrmin2  13181  ifle  13200  qbtwnxr  13203  xltnegi  13219  xleadd1a  13256  xlt2add  13263  xlemul1a  13291  xov1plusxeqvd  13502  elfzo0suble  13712  ubmelm1fzo  13769  flflp1  13817  ceim1l  13857  ceilm1lt  13858  ceille  13860  quoremz  13865  quoremnn0ALT  13867  modlt  13890  modeqmodmin  13954  addmodlteq  13959  seqf1olem1  14054  bernneq  14242  discr  14253  faclbnd2  14304  faclbnd4lem3  14308  hashun2  14396  hashfun  14450  hashf1dmcdm  14457  ccatsymb  14596  ccatrn  14603  sgnsub  15119  01sqrexlem6  15274  01sqrexlem7  15275  rddif  15368  amgm2  15397  icodiamlt  15465  climconst  15570  rlimconst  15571  serclim0  15604  rlimcn1  15615  mulcn2  15623  reccn2  15624  o1mul  15642  o1rlimmul  15646  iserex  15684  climlec2  15686  iserge0  15688  climcau  15698  caucvgrlem  15700  caucvgr  15703  iseraltlem2  15710  iseraltlem3  15711  iseralt  15712  fsumabs  15829  o1fsum  15841  iserabs  15843  climfsum  15848  isumless  15875  climcndslem2  15880  divrcnv  15882  flo1  15884  supcvg  15886  georeclim  15902  geomulcvg  15906  cvgrat  15913  mertenslem1  15914  prodfclim1  15923  fprodle  16026  efcvgfsum  16116  eftlub  16141  eflegeo  16153  tanhlt1  16192  tanhbnd  16193  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos01gt0  16223  ruclem2  16264  ruclem3  16265  ruclem9  16270  ruclem11  16272  ruclem12  16273  bitsfzolem  16468  bitsfzo  16469  bitsinv1lem  16475  sadcaddlem  16491  mulgcd  16582  eucalglt  16619  lcmledvds  16633  lcmfledvds  16666  mulgcddvds  16689  coprmproddvdslem  16696  prmind2  16719  isprm5  16742  divdenle  16784  nonsq  16794  pythagtriplem4  16855  pclem  16874  pcpremul  16879  pczdvds  16899  pcprmpw2  16918  qexpz  16937  prmreclem4  16955  prmreclem5  16956  4sqlem10  16983  ramtub  17048  ramub2  17050  prmodvdslcmf  17083  prmgaplem8  17094  natpropd  18012  catciso  18144  p0le  18459  acsdomd  18589  chnind  18653  chnub  18654  chnccat  18658  chnpolleha  18664  triv1nsgd  19214  qusgrp  19227  f1otrspeq  19487  pmtrfrn  19498  pmtrfconj  19506  symggen  19510  psgnunilem4  19537  oddvds2  19606  odcau  19644  pgpfi  19645  pgpssslw  19654  sylow3lem4  19670  efgred2  19793  frgp0  19800  odadd2  19889  oddvdssubg  19895  ablfac1c  20113  ablfac1eu  20115  pgpfaclem3  20125  2nsgsimpgd  20144  isabvd  20861  abvsubtri  20876  cyggic  21624  mplsubrg  22056  psdmplcl  22227  psdmul  22231  coe1sfi  22275  mp2pm2mplem5  22870  en2top  23045  1stcrest  23513  2ndcrest  23514  hausmapdom  23560  ufilen  23990  xmetrtri2  24416  prdsxmetlem  24428  bl2in  24460  xblcntrps  24470  xblcntr  24471  ssblps  24482  ssbl  24483  blssps  24484  blss  24485  blcld  24565  methaus  24580  metustexhalf  24616  nmtri2  24687  tngngp3  24716  nrginvrcnlem  24751  nrginvrcn  24752  nmoi  24788  nmo0  24795  nmoid  24802  blcvx  24858  reperflem  24879  reconnlem2  24888  metdcnlem  24897  metdscn  24917  metnrmlem3  24922  mulc1cncf  24967  iccpnfhmeo  25007  cnheiborlem  25016  cnheibor  25017  lebnumii  25028  pcopt  25084  pcopt2  25085  pcoass  25086  nmoleub2lem  25176  nmoleub2lem3  25177  nmoleub2lem2  25178  ipcau2  25296  tcphcphlem1  25297  nglmle  25364  trirn  25462  rrxdstprj1  25471  minveclem3  25491  ivthlem2  25514  ivthlem3  25515  ivth2  25517  ovollb  25541  ovolsslem  25546  ovollb2lem  25550  ovolctb  25552  ovoliunlem1  25564  ovolsca  25577  ovolicc1  25578  ovolicc2lem4  25582  nulmbl  25597  ioombl1lem4  25623  uniioovol  25641  uniioombllem3a  25646  uniioombllem4  25648  opnmbllem  25663  volcn  25668  volivth  25669  i1fadd  25757  i1fmul  25758  mbfi1fseqlem4  25780  mbfi1fseqlem5  25781  mbfi1fseqlem6  25782  itg2const2  25803  itg2seq  25804  itg2uba  25805  itg2split  25811  itg2monolem1  25812  itg2monolem3  25814  itg2i1fseq2  25818  itg2addlem  25820  itg2gt0  25822  itg2cnlem1  25823  itg2cnlem2  25824  itgless  25879  ibladdlem  25882  bddmulibl  25901  dveflem  26041  dvferm1lem  26046  dvferm2lem  26048  dvlip  26055  dvlipcn  26056  dvlip2  26057  dvle  26069  dvivthlem1  26070  lhop1lem  26075  dvcvx  26082  dvfsumabs  26085  dvfsumlem2  26089  dvfsumlem4  26091  dvfsumrlim2  26094  dvfsum2  26096  ftc1a  26099  ftc1lem4  26101  ftc1lem5  26102  deg1sub  26168  ply1divex  26197  deg1submon1p  26213  r1pdeglt  26220  dvdsq1p  26223  fta1glem2  26229  fta1g  26230  plyeq0lem  26270  dgrlt  26326  fta1lem  26371  aalioulem2  26397  aalioulem3  26398  aalioulem4  26399  aaliou3lem2  26407  aaliou3lem9  26414  taylply2  26431  ulmbdd  26461  ulmdvlem1  26463  mtest  26467  mtestbdd  26468  radcnvlem1  26476  radcnvle  26483  pserulm  26485  psercn  26489  pserdvlem2  26491  abelthlem2  26495  abelthlem5  26498  abelthlem7  26501  abelthlem8  26502  abelthlem9  26503  reeff1olem  26509  tangtx  26570  tanord  26603  efif1olem4  26610  logrnaddcl  26639  logcj  26671  logimul  26679  logneg2  26680  logdivlti  26685  divlogrlim  26700  logcnlem3  26709  logcnlem4  26710  efopn  26723  logtayllem  26724  logtayl  26725  cxpcn3lem  26812  cxpaddle  26817  abscxpbnd  26818  asinlem3  26936  asinneg  26951  asinsin  26957  atanlogaddlem  26978  atantan  26988  bndatandm  26994  atans2  26996  atantayl  27002  atantayl2  27003  atantayl3  27004  leibpi  27007  birthdaylem3  27018  rlimcnp  27030  efrlim  27034  cxplim  27036  cxp2lim  27041  cxploglim2  27043  divsqrtsumo1  27048  jensenlem2  27052  amgm  27055  logdifbnd  27058  harmonicbnd4  27075  fsumharmonic  27076  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem5  27097  lgambdd  27101  lgamcvg2  27119  ftalem1  27137  ftalem5  27141  basellem1  27145  basellem8  27152  ppip1le  27225  ppiltx  27241  sqff1o  27246  chtublem  27275  chpub  27284  logfaclbnd  27286  logfacrlim  27288  logexprlim  27289  mersenne  27291  bcmono  27341  bcmax  27342  bposlem2  27349  bposlem5  27352  lgslem3  27363  gausslemma2dlem1a  27429  lgsquadlem1  27444  lgsquadlem2  27445  2lgslem1c  27457  2sqblem  27495  chebbnd1  27536  chtppilimlem1  27537  chto1ub  27540  chpchtlim  27543  chpo1ubb  27545  rplogsumlem1  27548  rplogsumlem2  27549  rpvmasumlem  27551  dchrisumlem1  27553  dchrisumlem2  27554  dchrmusum2  27558  dchrvmasumlem2  27562  dchrvmasumlem3  27563  dchrvmasumiflem1  27565  dchrisum0flblem1  27572  dchrisum0fno1  27575  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2a  27581  dchrisum0lem2  27582  rplogsum  27591  mudivsum  27594  mulogsumlem  27595  mulog2sumlem1  27598  mulog2sumlem2  27599  vmalogdivsum2  27602  2vmadivsumlem  27604  selberglem2  27610  selberg2b  27616  logdivbnd  27620  selberg3lem1  27621  selberg3lem2  27622  selberg4lem1  27624  pntrmax  27628  pntrsumo1  27629  pntrlog2bndlem1  27641  pntrlog2bndlem2  27642  pntrlog2bndlem3  27643  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntrlog2bnd  27648  pntpbnd1a  27649  pntpbnd2  27651  pntibndlem2  27655  pntlemb  27661  pntlemg  27662  pntlemh  27663  pntlemr  27666  pntlemj  27667  pntlemf  27669  pntlemo  27671  pnt  27678  padicabv  27694  ostth2lem2  27698  ostth2lem3  27699  ostth3  27702  nosep1o  27745  nodense  27756  noinfbnd2lem1  27794  noetainflem3  27803  mins1  27835  mins2  27836  eqcuts3  27897  cofcutr  28017  cofcutrtime  28020  addsuniflem  28094  negsunif  28148  sltmuls1  28240  mulsuniflem  28242  precsexlem11  28310  halfcut  28551  pw2cut  28553  bdayfinbndlem1  28560  recut  28587  elreno2  28588  readdscl  28592  remulscllem2  28594  colperpexlem3  28905  mideulem2  28907  lnperpex  28976  trgcopy  28977  iscgra1  29004  brbtwn2  29106  colinearalglem4  29110  subupgr  29488  crctcshwlkn0lem1  30010  nvabs  30875  nvge0  30876  smcnlem  30900  nmblolbii  31002  blocnilem  31007  siii  31056  ubthlem2  31074  minvecolem3  31079  htthlem  31120  bcsiALT  31382  bcs3  31386  chscllem4  31843  0cnop  32182  0cnfn  32183  nmbdoplbi  32227  nmcoplbi  32231  nmophmi  32234  nmbdfnlbi  32252  nmcfnlbi  32255  nlelchi  32264  riesz1  32268  cnlnadjlem2  32271  nmopadjlei  32291  nmoptrii  32297  nmopcoi  32298  nmopcoadji  32304  unierri  32307  branmfn  32308  pjs14i  32413  hstle  32433  cdj3lem2b  32640  xlt2addrd  32961  eliccelico  32979  elicoelioo  32980  ltesubnnd  33025  2exple2exp  33036  oexpled  33038  wrdt2ind  33131  archirngz  33369  archiabllem2c  33375  dflring3  33693  dflring4  33694  evl1deg1  33772  evl1deg2  33773  evl1deg3  33774  ply1degltel  33790  ply1degleel  33791  ig1pmindeg  33798  q1pdir  33799  selvply1rhmlema  33815  extvfvcl  33833  mplvrpmfgalem  33841  esplympl  33864  esplyind  33872  vietadeg1  33875  lbslelsp  33895  ply1degltdimlem  33919  fldextrspunlem1  33972  fldextrspundgle  33975  minplymindeg  34005  minplyirredlem  34007  irredminply  34013  algextdeglem6  34019  rtelextdg2lem  34023  cos9thpiminplylem1  34079  madjusmdetlem2  34125  locfinref  34138  sqsscirc1  34205  tpr2rico  34209  esumcst  34360  esumgect  34387  esum2d  34390  measunl  34513  measiun  34515  omssubaddlem  34596  omssubadd  34597  carsgsigalem  34612  carsgclctunlem2  34616  pmeasmono  34621  eulerpartlemgc  34659  eulerpartlemb  34665  ballotlemsel1i  34810  ballotlemro  34820  signsplypnf  34844  signsply0  34845  signsvtn  34878  signsvfnn  34880  hgt750lemd  34942  logdivsqrle  34944  erdsze2lem1  35553  sinccvglem  36022  divcnvlin  36083  iprodefisum  36091  faclimlem2  36094  fnemeet1  36726  weiunpo  36825  dnibndlem10  36925  dnibndlem11  36926  dnibnd  36929  knoppcnlem4  36934  knoppcnlem6  36936  unblimceq0lem  36944  unbdqndv2lem1  36947  unbdqndv2lem2  36948  knoppndvlem11  36960  knoppndvlem12  36961  knoppndvlem14  36963  knoppndvlem15  36964  knoppndvlem17  36966  knoppndvlem18  36967  knoppndvlem19  36968  knoppndvlem21  36970  ctbssinf  37900  ltflcei  38107  ptrecube  38119  poimirlem16  38135  poimirlem17  38136  poimirlem29  38148  broucube  38153  opnmbllem0  38155  mblfinlem2  38157  mblfinlem3  38158  ismblfin  38160  itg2addnclem  38170  itg2addnclem2  38171  itg2addnclem3  38172  itg2addnc  38173  ibladdnclem  38175  ftc1cnnclem  38190  ftc1cnnc  38191  ftc1anc  38200  geomcau  38258  prdsbnd  38292  cntotbnd  38295  heiborlem4  38313  rrndstprj2  38330  rrncmslem  38331  rrnequiv  38334  iccbnd  38339  cvlcvr1  39963  cvrat3  40066  dalem25  40322  cdlema1N  40415  dalawlem3  40497  dalawlem4  40498  dalawlem5  40499  dalawlem6  40500  dalawlem7  40501  dalawlem9  40503  dalawlem11  40505  dalawlem12  40506  lhp2lt  40625  lhpmcvr  40647  4atexlemcnd  40696  lautj  40717  trlle  40808  trlval3  40811  trlval4  40812  cdleme0moN  40849  cdleme13  40896  cdleme15  40902  cdleme19b  40928  cdleme20e  40937  cdleme20j  40942  cdleme22e  40968  cdleme22eALTN  40969  cdleme26fALTN  40986  cdleme26f  40987  cdleme27N  40993  cdleme41sn3a  41057  cdleme46fsvlpq  41129  cdlemeg46vrg  41151  cdlemg4  41241  cdlemg7N  41250  cdlemg9a  41256  cdlemg11b  41266  cdlemg12a  41267  trljco  41364  tendoidcl  41393  tendococl  41396  tendopltp  41404  tendo0tp  41413  tendoicl  41420  cdlemi2  41443  cdlemk5a  41459  cdlemk5  41460  cdlemk12  41474  cdlemkole  41477  cdlemk14  41478  cdlemk12u  41496  cdlemk37  41538  cdlemk39s-id  41564  cdlemk49  41575  cdlemk39u1  41591  cdlemk39u  41592  dian0  41663  cdlemm10N  41742  cdlemn2  41819  cdlemn10  41830  dihord1  41842  dihord10  41847  dihmeetlem4preN  41930  dihmeetlem18N  41948  dihmeetlem20N  41950  dihjatc  42041  mapdcnvatN  42290  lcmineqlem17  42662  3lexlogpow5ineq2  42672  3lexlogpow2ineq2  42676  3lexlogpow5ineq5  42677  aks4d1p1p3  42686  aks4d1p1p2  42687  aks4d1p1p4  42688  aks4d1p1p7  42691  aks4d1p1p5  42692  aks4d1p1  42693  aks4d1p3  42695  aks4d1p5  42697  aks4d1p6  42698  aks4d1p7d1  42699  aks4d1p7  42700  aks4d1p8  42704  isprimroot2  42711  posbezout  42717  primrootspoweq0  42723  aks6d1c1p8  42732  aks6d1c1  42733  hashscontpow1  42738  aks6d1c2lem4  42744  aks6d1c2  42747  aks6d1c5lem1  42753  aks6d1c5lem3  42754  2ap1caineq  42762  sticksstones7  42769  sticksstones10  42772  sticksstones11  42773  sticksstones12a  42774  sticksstones12  42775  sticksstones22  42785  aks6d1c6lem2  42788  aks6d1c6lem3  42789  aks6d1c6lem4  42790  aks6d1c6lem5  42794  bcled  42795  bcle2d  42796  aks6d1c7lem1  42797  aks6d1c7lem2  42798  aks5lem3a  42806  unitscyglem1  42812  unitscyglem4  42815  unitscyglem5  42816  aks5  42821  sn-reclt0d  43103  evlselv  43171  fltltc  43243  lzenom  43351  irrapxlem2  43400  irrapxlem3  43401  irrapxlem5  43403  pellexlem2  43407  pell14qrgt0  43436  pellfundlb  43461  pellfundex  43463  pellfund14  43475  rmspecsqrtnq  43483  jm2.24nn  43536  jm2.17a  43537  jm2.17b  43538  congabseq  43551  acongrep  43557  acongeq  43560  jm2.26lem3  43578  jm2.27a  43582  jm2.27c  43584  hbtlem2  43701  dgraaub  43725  idomodle  43768  safesnsupfidom1o  43993  sqrtcval  44217  relexpxpmin  44293  frege102d  44330  hashnzfzclim  44898  binomcxplemfrat  44927  binomcxplemnotnn0  44932  suprnmpt  45752  mpct  45778  rnmptbddlem  45819  dstregt0  45861  lefldiveq  45871  fzisoeu  45879  upbdrech  45884  ssfiunibd  45888  fzdifsuc2  45889  xadd0ge  45898  supxrgere  45909  supxrge  45914  suplesup  45915  xrlexaddrp  45928  infxrunb2  45943  infleinflem2  45946  reclt0d  45962  infrpgernmpt  46039  rexanuz2nf  46066  ioondisj2  46069  iccshift  46094  iooshift  46098  fmul01  46156  fmul01lt1lem1  46160  fmul01lt1lem2  46161  climrec  46179  climsuse  46184  mullimc  46192  mullimcf  46199  constlimc  46200  idlimc  46202  divcnvg  46203  limcperiod  46204  limcrecl  46205  lptioo2  46207  lptioo1  46208  islpcn  46213  lptre2pt  46214  limcleqr  46218  neglimc  46221  addlimc  46222  0ellimcdiv  46223  limclner  46225  climleltrp  46250  limsuplesup  46273  limsupmnflem  46294  supcnvlimsupmpt  46315  0cnv  46316  xlimconst  46399  xlimliminflimsup  46436  sinaover2ne0  46442  cncfshift  46448  cncfperiod  46453  cncfioobdlem  46470  cncfioobd  46471  fperdvper  46493  dvdivbd  46497  dvbdfbdioolem1  46502  dvbdfbdioolem2  46503  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnmul  46517  dvnprodlem1  46520  itgiccshift  46554  itgperiod  46555  ismbl3  46560  ovolsplit  46562  stoweidlem1  46575  stoweidlem11  46585  stoweidlem13  46587  stoweidlem14  46588  stoweidlem16  46590  stoweidlem21  46595  stoweidlem25  46599  stoweidlem26  46600  stoweidlem36  46610  stoweidlem38  46612  stoweidlem41  46615  stoweidlem42  46616  stoweidlem45  46619  stoweidlem48  46622  stoweidlem52  46626  stoweidlem62  46636  wallispilem3  46641  stirlinglem5  46652  stirlinglem6  46653  stirlinglem7  46654  stirlinglem10  46657  stirlinglem12  46659  stirlinglem15  46662  dirkercncflem1  46677  fourierdlem10  46691  fourierdlem12  46693  fourierdlem15  46696  fourierdlem16  46697  fourierdlem19  46700  fourierdlem20  46701  fourierdlem21  46702  fourierdlem22  46703  fourierdlem24  46705  fourierdlem30  46711  fourierdlem37  46718  fourierdlem39  46720  fourierdlem40  46721  fourierdlem41  46722  fourierdlem42  46723  fourierdlem47  46727  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem52  46732  fourierdlem54  46734  fourierdlem60  46740  fourierdlem61  46741  fourierdlem63  46743  fourierdlem64  46744  fourierdlem68  46748  fourierdlem71  46751  fourierdlem72  46752  fourierdlem73  46753  fourierdlem74  46754  fourierdlem75  46755  fourierdlem76  46756  fourierdlem77  46757  fourierdlem78  46758  fourierdlem79  46759  fourierdlem81  46761  fourierdlem82  46762  fourierdlem83  46763  fourierdlem84  46764  fourierdlem87  46767  fourierdlem92  46772  fourierdlem93  46773  fourierdlem94  46774  fourierdlem101  46781  fourierdlem102  46782  fourierdlem103  46783  fourierdlem104  46784  fourierdlem111  46791  fourierdlem112  46792  fourierdlem113  46793  fourierdlem114  46794  sqwvfoura  46802  sqwvfourb  46803  fouriersw  46805  elaa2lem  46807  etransclem23  46831  etransclem28  46836  etransclem32  46840  etransclem35  46843  etransclem48  46856  qndenserrnbllem  46868  rrnprjdstle  46875  ioorrnopnlem  46878  ioorrnopnxrlem  46880  salexct  46908  sge0fsum  46961  sge0supre  46963  sge0rnbnd  46967  sge0lefi  46972  sge0lessmpt  46973  sge0ltfirp  46974  sge0prle  46975  sge0resrnlem  46977  sge0le  46981  sge0split  46983  sge0iunmptlemre  46989  sge0iunmpt  46992  sge0isum  47001  sge0xaddlem1  47007  sge0xaddlem2  47008  sge0xadd  47009  sge0reuz  47021  sge0reuzb  47022  meaunle  47038  meaiunlelem  47042  voliunsge0lem  47046  meaiuninc  47055  meaiininclem  47060  omeunle  47090  omeiunle  47091  omelesplit  47092  omeiunltfirp  47093  carageniuncllem2  47096  caratheodorylem2  47101  caragencmpl  47109  ovnlecvr  47132  ovncvrrp  47138  ovnsubaddlem1  47144  ovnsubadd  47146  hoidmv1lelem1  47165  hoidmv1lelem2  47166  hoidmv1le  47168  hoidmvlelem1  47169  hoidmvlelem2  47170  hoidmvlelem5  47173  hoidmvle  47174  ovnhoilem1  47175  ovnlecvr2  47184  ovncvr2  47185  hoiqssbllem2  47197  hspmbllem2  47201  hspmbllem3  47202  ovnsplit  47222  ovolval5lem1  47226  vonioolem1  47254  vonioolem2  47255  vonicclem1  47257  vonicclem2  47258  pimconstlt1  47276  smflimlem2  47346  smflimlem4  47348  smfmullem1  47365  smfsuplem1  47385  smflimsuplem4  47397  smflimsuplem5  47398  chnerlem1  47458  chner  47461  difmodm1lt  47959  2timesltsqm1  47973  iccpartltu  48031  iccpartleu  48034  pgrple2abl  48987  nnpw2blen  49202  dignn0flhalflem1  49237  2itscp  49403  functermclem  50128