Theorem eqbrtrd 5094

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  eqbrtrrd  5096  somin2  6085  en1b  8962  domunsncan  9005  fodomfi  9212  fodomfiOLD  9230  infsupprpr  9409  hartogslem1  9447  wemaplem2  9452  infdifsn  9569  ttrclselem2  9638  carddomi2  9885  djuinf  10102  carden  10464  alephsuc3  10494  fpwwe2lem5  10549  fpwwe2lem6  10550  inar1  10689  rankcf  10691  lesub3d  11759  lbinfle  12102  supadd  12115  supmul  12119  rpnnen1lem3  12920  divge1  13003  xrmin1  13120  xrmin2  13121  ifle  13140  qbtwnxr  13143  xltnegi  13159  xleadd1a  13196  xlt2add  13203  xlemul1a  13231  xov1plusxeqvd  13442  elfzo0suble  13652  ubmelm1fzo  13709  flflp1  13757  ceim1l  13797  ceilm1lt  13798  ceille  13800  quoremz  13805  quoremnn0ALT  13807  modlt  13830  modeqmodmin  13894  addmodlteq  13899  seqf1olem1  13994  bernneq  14182  discr  14193  faclbnd2  14244  faclbnd4lem3  14248  hashun2  14336  hashfun  14390  hashf1dmcdm  14397  ccatsymb  14536  ccatrn  14543  01sqrexlem6  15200  01sqrexlem7  15201  rddif  15294  amgm2  15323  icodiamlt  15391  climconst  15496  rlimconst  15497  serclim0  15530  rlimcn1  15541  mulcn2  15549  reccn2  15550  o1mul  15568  o1rlimmul  15572  iserex  15610  climlec2  15612  iserge0  15614  climcau  15624  caucvgrlem  15626  caucvgr  15629  iseraltlem2  15636  iseraltlem3  15637  iseralt  15638  fsumabs  15755  o1fsum  15767  iserabs  15769  climfsum  15774  isumless  15801  climcndslem2  15806  divrcnv  15808  flo1  15810  supcvg  15812  georeclim  15828  geomulcvg  15832  cvgrat  15839  mertenslem1  15840  prodfclim1  15849  fprodle  15952  efcvgfsum  16042  eftlub  16067  eflegeo  16079  tanhlt1  16118  tanhbnd  16119  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos01gt0  16149  ruclem2  16190  ruclem3  16191  ruclem9  16196  ruclem11  16198  ruclem12  16199  bitsfzolem  16394  bitsfzo  16395  bitsinv1lem  16401  sadcaddlem  16417  mulgcd  16508  eucalglt  16545  lcmledvds  16559  lcmfledvds  16592  mulgcddvds  16615  coprmproddvdslem  16622  prmind2  16645  isprm5  16668  divdenle  16710  nonsq  16720  pythagtriplem4  16781  pclem  16800  pcpremul  16805  pczdvds  16825  pcprmpw2  16844  qexpz  16863  prmreclem4  16881  prmreclem5  16882  4sqlem10  16909  ramtub  16974  ramub2  16976  prmodvdslcmf  17009  prmgaplem8  17020  natpropd  17937  catciso  18069  p0le  18384  acsdomd  18514  chnind  18578  chnub  18579  chnccat  18583  chnpolleha  18589  triv1nsgd  19139  qusgrp  19152  f1otrspeq  19413  pmtrfrn  19424  pmtrfconj  19432  symggen  19436  psgnunilem4  19463  oddvds2  19532  odcau  19570  pgpfi  19571  pgpssslw  19580  sylow3lem4  19596  efgred2  19719  frgp0  19726  odadd2  19815  oddvdssubg  19821  ablfac1c  20039  ablfac1eu  20041  pgpfaclem3  20051  2nsgsimpgd  20070  isabvd  20784  abvsubtri  20799  cyggic  21547  mplsubrg  21979  psdmplcl  22150  psdmul  22154  coe1sfi  22198  mp2pm2mplem5  22793  en2top  22968  1stcrest  23436  2ndcrest  23437  hausmapdom  23483  ufilen  23913  xmetrtri2  24339  prdsxmetlem  24351  bl2in  24383  xblcntrps  24393  xblcntr  24394  ssblps  24405  ssbl  24406  blssps  24407  blss  24408  blcld  24488  methaus  24503  metustexhalf  24539  nmtri2  24610  tngngp3  24639  nrginvrcnlem  24674  nrginvrcn  24675  nmoi  24711  nmo0  24718  nmoid  24725  blcvx  24781  reperflem  24802  reconnlem2  24811  metdcnlem  24820  metdscn  24840  metnrmlem3  24845  mulc1cncf  24890  iccpnfhmeo  24930  cnheiborlem  24939  cnheibor  24940  lebnumii  24951  pcopt  25007  pcopt2  25008  pcoass  25009  nmoleub2lem  25099  nmoleub2lem3  25100  nmoleub2lem2  25101  ipcau2  25219  tcphcphlem1  25220  nglmle  25287  trirn  25385  rrxdstprj1  25394  minveclem3  25414  ivthlem2  25437  ivthlem3  25438  ivth2  25440  ovollb  25464  ovolsslem  25469  ovollb2lem  25473  ovolctb  25475  ovoliunlem1  25487  ovolsca  25500  ovolicc1  25501  ovolicc2lem4  25505  nulmbl  25520  ioombl1lem4  25546  uniioovol  25564  uniioombllem3a  25569  uniioombllem4  25571  opnmbllem  25586  volcn  25591  volivth  25592  i1fadd  25680  i1fmul  25681  mbfi1fseqlem4  25703  mbfi1fseqlem5  25704  mbfi1fseqlem6  25705  itg2const2  25726  itg2seq  25727  itg2uba  25728  itg2split  25734  itg2monolem1  25735  itg2monolem3  25737  itg2i1fseq2  25741  itg2addlem  25743  itg2gt0  25745  itg2cnlem1  25746  itg2cnlem2  25747  itgless  25802  ibladdlem  25805  bddmulibl  25824  dveflem  25964  dvferm1lem  25969  dvferm2lem  25971  dvlip  25978  dvlipcn  25979  dvlip2  25980  dvle  25992  dvivthlem1  25993  lhop1lem  25998  dvcvx  26005  dvfsumabs  26008  dvfsumlem2  26012  dvfsumlem4  26014  dvfsumrlim2  26017  dvfsum2  26019  ftc1a  26022  ftc1lem4  26024  ftc1lem5  26025  deg1sub  26091  ply1divex  26120  deg1submon1p  26136  r1pdeglt  26143  dvdsq1p  26146  fta1glem2  26152  fta1g  26153  plyeq0lem  26193  dgrlt  26249  fta1lem  26291  aalioulem2  26317  aalioulem3  26318  aalioulem4  26319  aaliou3lem2  26327  aaliou3lem9  26334  taylply2  26351  ulmbdd  26381  ulmdvlem1  26383  mtest  26387  mtestbdd  26388  radcnvlem1  26396  radcnvle  26403  pserulm  26405  psercn  26409  pserdvlem2  26411  abelthlem2  26415  abelthlem5  26418  abelthlem7  26421  abelthlem8  26422  abelthlem9  26423  reeff1olem  26429  tangtx  26487  tanord  26520  efif1olem4  26527  logrnaddcl  26556  logcj  26588  logimul  26596  logneg2  26597  logdivlti  26602  divlogrlim  26617  logcnlem3  26626  logcnlem4  26627  efopn  26640  logtayllem  26641  logtayl  26642  cxpcn3lem  26729  cxpaddle  26734  abscxpbnd  26735  asinlem3  26853  asinneg  26868  asinsin  26874  atanlogaddlem  26895  atantan  26905  bndatandm  26911  atans2  26913  atantayl  26919  atantayl2  26920  atantayl3  26921  leibpi  26924  birthdaylem3  26935  rlimcnp  26947  efrlim  26951  cxplim  26953  cxp2lim  26958  cxploglim2  26960  divsqrtsumo1  26965  jensenlem2  26969  amgm  26972  logdifbnd  26975  harmonicbnd4  26992  fsumharmonic  26993  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgambdd  27018  lgamcvg2  27036  ftalem1  27054  ftalem5  27058  basellem1  27062  basellem8  27069  ppip1le  27142  ppiltx  27158  sqff1o  27163  chtublem  27192  chpub  27201  logfaclbnd  27203  logfacrlim  27205  logexprlim  27206  mersenne  27208  bcmono  27258  bcmax  27259  bposlem2  27266  bposlem5  27269  lgslem3  27280  gausslemma2dlem1a  27346  lgsquadlem1  27361  lgsquadlem2  27362  2lgslem1c  27374  2sqblem  27412  chebbnd1  27453  chtppilimlem1  27454  chto1ub  27457  chpchtlim  27460  chpo1ubb  27462  rplogsumlem1  27465  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0fno1  27492  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  rplogsum  27508  mudivsum  27511  mulogsumlem  27512  mulog2sumlem1  27515  mulog2sumlem2  27516  vmalogdivsum2  27519  2vmadivsumlem  27521  selberglem2  27527  selberg2b  27533  logdivbnd  27537  selberg3lem1  27538  selberg3lem2  27539  selberg4lem1  27541  pntrmax  27545  pntrsumo1  27546  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd2  27568  pntibndlem2  27572  pntlemb  27578  pntlemg  27579  pntlemh  27580  pntlemr  27583  pntlemj  27584  pntlemf  27586  pntlemo  27588  pnt  27595  padicabv  27611  ostth2lem2  27615  ostth2lem3  27616  ostth3  27619  nosep1o  27663  nodense  27674  noinfbnd2lem1  27712  noetainflem3  27721  mins1  27753  mins2  27754  eqcuts3  27814  cofcutr  27934  cofcutrtime  27937  addsuniflem  28011  negsunif  28065  sltmuls1  28157  mulsuniflem  28159  precsexlem11  28227  halfcut  28468  pw2cut  28470  bdayfinbndlem1  28477  recut  28504  elreno2  28505  readdscl  28509  remulscllem2  28511  colperpexlem3  28818  mideulem2  28820  lnperpex  28889  trgcopy  28890  iscgra1  28896  brbtwn2  28992  colinearalglem4  28996  subupgr  29374  crctcshwlkn0lem1  29896  nvabs  30761  nvge0  30762  smcnlem  30786  nmblolbii  30888  blocnilem  30893  siii  30942  ubthlem2  30960  minvecolem3  30965  htthlem  31006  bcsiALT  31268  bcs3  31272  chscllem4  31729  0cnop  32068  0cnfn  32069  nmbdoplbi  32113  nmcoplbi  32117  nmophmi  32120  nmbdfnlbi  32138  nmcfnlbi  32141  nlelchi  32150  riesz1  32154  cnlnadjlem2  32157  nmopadjlei  32177  nmoptrii  32183  nmopcoi  32184  nmopcoadji  32190  unierri  32193  branmfn  32194  pjs14i  32299  hstle  32319  cdj3lem2b  32526  xlt2addrd  32851  eliccelico  32869  elicoelioo  32870  ltesubnnd  32915  sgnsub  32929  2exple2exp  32937  oexpled  32939  wrdt2ind  33032  archirngz  33270  archiabllem2c  33276  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ply1degltel  33677  ply1degleel  33678  ig1pmindeg  33685  q1pdir  33686  selvply1rhmlema  33702  extvfvcl  33720  mplvrpmfgalem  33728  esplympl  33751  esplyind  33759  vietadeg1  33762  lbslelsp  33782  ply1degltdimlem  33806  fldextrspunlem1  33859  fldextrspundgle  33862  minplymindeg  33892  minplyirredlem  33894  irredminply  33900  algextdeglem6  33906  rtelextdg2lem  33910  cos9thpiminplylem1  33966  madjusmdetlem2  34012  locfinref  34025  sqsscirc1  34092  tpr2rico  34096  esumcst  34247  esumgect  34274  esum2d  34277  measunl  34400  measiun  34402  omssubaddlem  34483  omssubadd  34484  carsgsigalem  34499  carsgclctunlem2  34503  pmeasmono  34508  eulerpartlemgc  34546  eulerpartlemb  34552  ballotlemsel1i  34697  ballotlemro  34707  signsplypnf  34734  signsply0  34735  signsvtn  34768  signsvfnn  34770  hgt750lemd  34832  logdivsqrle  34834  erdsze2lem1  35431  sinccvglem  35900  divcnvlin  35961  iprodefisum  35969  faclimlem2  35972  fnemeet1  36594  weiunpo  36693  dnibndlem10  36793  dnibndlem11  36794  dnibnd  36797  knoppcnlem4  36802  knoppcnlem6  36804  unblimceq0lem  36812  unbdqndv2lem1  36815  unbdqndv2lem2  36816  knoppndvlem11  36828  knoppndvlem12  36829  knoppndvlem14  36831  knoppndvlem15  36832  knoppndvlem17  36834  knoppndvlem18  36835  knoppndvlem19  36836  knoppndvlem21  36838  ctbssinf  37768  ltflcei  37975  ptrecube  37987  poimirlem16  38003  poimirlem17  38004  poimirlem29  38016  broucube  38021  opnmbllem0  38023  mblfinlem2  38025  mblfinlem3  38026  ismblfin  38028  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  ibladdnclem  38043  ftc1cnnclem  38058  ftc1cnnc  38059  ftc1anc  38068  geomcau  38126  prdsbnd  38160  cntotbnd  38163  heiborlem4  38181  rrndstprj2  38198  rrncmslem  38199  rrnequiv  38202  iccbnd  38207  cvlcvr1  39831  cvrat3  39934  dalem25  40190  cdlema1N  40283  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  lhp2lt  40493  lhpmcvr  40515  4atexlemcnd  40564  lautj  40585  trlle  40676  trlval3  40679  trlval4  40680  cdleme0moN  40717  cdleme13  40764  cdleme15  40770  cdleme19b  40796  cdleme20e  40805  cdleme20j  40810  cdleme22e  40836  cdleme22eALTN  40837  cdleme26fALTN  40854  cdleme26f  40855  cdleme27N  40861  cdleme41sn3a  40925  cdleme46fsvlpq  40997  cdlemeg46vrg  41019  cdlemg4  41109  cdlemg7N  41118  cdlemg9a  41124  cdlemg11b  41134  cdlemg12a  41135  trljco  41232  tendoidcl  41261  tendococl  41264  tendopltp  41272  tendo0tp  41281  tendoicl  41288  cdlemi2  41311  cdlemk5a  41327  cdlemk5  41328  cdlemk12  41342  cdlemkole  41345  cdlemk14  41346  cdlemk12u  41364  cdlemk37  41406  cdlemk39s-id  41432  cdlemk49  41443  cdlemk39u1  41459  cdlemk39u  41460  dian0  41531  cdlemm10N  41610  cdlemn2  41687  cdlemn10  41698  dihord1  41710  dihord10  41715  dihmeetlem4preN  41798  dihmeetlem18N  41816  dihmeetlem20N  41818  dihjatc  41909  mapdcnvatN  42158  lcmineqlem17  42530  3lexlogpow5ineq2  42540  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1p3  42554  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p3  42563  aks4d1p5  42565  aks4d1p6  42566  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  isprimroot2  42579  posbezout  42585  primrootspoweq0  42591  aks6d1c1p8  42600  aks6d1c1  42601  hashscontpow1  42606  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c5lem1  42621  aks6d1c5lem3  42622  2ap1caineq  42630  sticksstones7  42637  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones12  42643  sticksstones22  42653  aks6d1c6lem2  42656  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6lem5  42662  bcled  42663  bcle2d  42664  aks6d1c7lem1  42665  aks6d1c7lem2  42666  aks5lem3a  42674  unitscyglem1  42680  unitscyglem4  42683  unitscyglem5  42684  aks5  42689  sn-reclt0d  42971  evlselv  43039  fltltc  43111  lzenom  43219  irrapxlem2  43268  irrapxlem3  43269  irrapxlem5  43271  pellexlem2  43275  pell14qrgt0  43304  pellfundlb  43329  pellfundex  43331  pellfund14  43343  rmspecsqrtnq  43351  jm2.24nn  43404  jm2.17a  43405  jm2.17b  43406  congabseq  43419  acongrep  43425  acongeq  43428  jm2.26lem3  43446  jm2.27a  43450  jm2.27c  43452  hbtlem2  43569  dgraaub  43593  idomodle  43636  safesnsupfidom1o  43861  sqrtcval  44085  relexpxpmin  44161  frege102d  44198  hashnzfzclim  44766  binomcxplemfrat  44795  binomcxplemnotnn0  44800  suprnmpt  45621  mpct  45647  rnmptbddlem  45688  dstregt0  45730  lefldiveq  45740  fzisoeu  45748  upbdrech  45753  ssfiunibd  45757  fzdifsuc2  45758  xadd0ge  45767  supxrgere  45778  supxrge  45783  suplesup  45784  xrlexaddrp  45797  infxrunb2  45812  infleinflem2  45815  reclt0d  45831  infrpgernmpt  45908  rexanuz2nf  45935  ioondisj2  45938  iccshift  45963  iooshift  45967  fmul01  46025  fmul01lt1lem1  46029  fmul01lt1lem2  46030  climrec  46048  climsuse  46053  mullimc  46061  mullimcf  46068  constlimc  46069  idlimc  46071  divcnvg  46072  limcperiod  46073  limcrecl  46074  lptioo2  46076  lptioo1  46077  islpcn  46082  lptre2pt  46083  limcleqr  46087  neglimc  46090  addlimc  46091  0ellimcdiv  46092  limclner  46094  climleltrp  46119  limsuplesup  46142  limsupmnflem  46163  supcnvlimsupmpt  46184  0cnv  46185  xlimconst  46268  xlimliminflimsup  46305  sinaover2ne0  46311  cncfshift  46317  cncfperiod  46322  cncfioobdlem  46339  cncfioobd  46340  fperdvper  46362  dvdivbd  46366  dvbdfbdioolem1  46371  dvbdfbdioolem2  46372  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  dvnprodlem1  46389  itgiccshift  46423  itgperiod  46424  ismbl3  46429  ovolsplit  46431  stoweidlem1  46444  stoweidlem11  46454  stoweidlem13  46456  stoweidlem14  46457  stoweidlem16  46459  stoweidlem21  46464  stoweidlem25  46468  stoweidlem26  46469  stoweidlem36  46479  stoweidlem38  46481  stoweidlem41  46484  stoweidlem42  46485  stoweidlem45  46488  stoweidlem48  46491  stoweidlem52  46495  stoweidlem62  46505  wallispilem3  46510  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem10  46526  stirlinglem12  46528  stirlinglem15  46531  dirkercncflem1  46546  fourierdlem10  46560  fourierdlem12  46562  fourierdlem15  46565  fourierdlem16  46566  fourierdlem19  46569  fourierdlem20  46570  fourierdlem21  46571  fourierdlem22  46572  fourierdlem24  46574  fourierdlem30  46580  fourierdlem37  46587  fourierdlem39  46589  fourierdlem40  46590  fourierdlem41  46591  fourierdlem42  46592  fourierdlem47  46596  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem52  46601  fourierdlem54  46603  fourierdlem60  46609  fourierdlem61  46610  fourierdlem63  46612  fourierdlem64  46613  fourierdlem68  46617  fourierdlem71  46620  fourierdlem72  46621  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem77  46626  fourierdlem78  46627  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem83  46632  fourierdlem84  46633  fourierdlem87  46636  fourierdlem92  46641  fourierdlem93  46642  fourierdlem94  46643  fourierdlem101  46650  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fourierdlem114  46663  sqwvfoura  46671  sqwvfourb  46672  fouriersw  46674  elaa2lem  46676  etransclem23  46700  etransclem28  46705  etransclem32  46709  etransclem35  46712  etransclem48  46725  qndenserrnbllem  46737  rrnprjdstle  46744  ioorrnopnlem  46747  ioorrnopnxrlem  46749  salexct  46777  sge0fsum  46830  sge0supre  46832  sge0rnbnd  46836  sge0lefi  46841  sge0lessmpt  46842  sge0ltfirp  46843  sge0prle  46844  sge0resrnlem  46846  sge0le  46850  sge0split  46852  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0isum  46870  sge0xaddlem1  46876  sge0xaddlem2  46877  sge0xadd  46878  sge0reuz  46890  sge0reuzb  46891  meaunle  46907  meaiunlelem  46911  voliunsge0lem  46915  meaiuninc  46924  meaiininclem  46929  omeunle  46959  omeiunle  46960  omelesplit  46961  omeiunltfirp  46962  carageniuncllem2  46965  caratheodorylem2  46970  caragencmpl  46978  ovnlecvr  47001  ovncvrrp  47007  ovnsubaddlem1  47013  ovnsubadd  47015  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem5  47042  hoidmvle  47043  ovnhoilem1  47044  ovnlecvr2  47053  ovncvr2  47054  hoiqssbllem2  47066  hspmbllem2  47070  hspmbllem3  47071  ovnsplit  47091  ovolval5lem1  47095  vonioolem1  47123  vonioolem2  47124  vonicclem1  47126  vonicclem2  47127  pimconstlt1  47145  smflimlem2  47215  smflimlem4  47217  smfmullem1  47234  smfsuplem1  47254  smflimsuplem4  47266  smflimsuplem5  47267  chnerlem1  47327  chner  47330  difmodm1lt  47828  2timesltsqm1  47842  iccpartltu  47900  iccpartleu  47903  pgrple2abl  48856  nnpw2blen  49071  dignn0flhalflem1  49106  2itscp  49272  functermclem  49997