Theorem breq2 5109

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

Assertion

Ref	Expression
breq2	⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 4835	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2850	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 5106	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 5106	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  ⟨cop 4591   class class class wbr 5105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106

This theorem is referenced by:  breq12  5110  breq2i  5113  breq2d  5117  nbrne1  5124  brralrspcev  5165  brimralrspcev  5166  pocl  5568  swopolem  5570  swopo  5571  solin  5587  sotric  5590  sotrieq  5591  isso2i  5597  somo  5599  sotr3  5601  seex  5611  frirr  5628  fr2nr  5629  frminex  5631  wereu2  5649  vtoclr  5715  posn  5738  frsn  5740  brcog  5843  brcogw  5845  brcnvg  5856  dfdmf  5877  breldmg  5890  dm0rn0  5905  dfrnf  5931  dmcoss  5956  dmcossOLD  5957  dmcosseq  5959  dmcosseqOLD  5960  resieq  5980  dfres2  6034  elimag  6057  relimasn  6078  elrelimasn  6079  cotrg  6102  cnvsym  6105  asymref2  6108  intirr  6109  poirr2  6115  sotri3  6121  poltletr  6123  soltmin  6127  rnco  6243  dfpo2  6287  dfpred3g  6304  predtrss  6313  frpomin  6331  dffun2  6535  dffun6  6536  dffun6f  6540  fun11  6599  tz6.12-2  6858  brprcneu  6861  brprcneuALT  6862  fv3  6889  tz6.12i  6897  funbrfv  6919  fnbrfvb  6921  funfv2f  6960  dffv2  6966  fvopab5  7013  fndmdif  7027  dff3  7085  fmptco  7115  foeqcnvco  7288  isorel  7314  soisores  7315  soisoi  7316  isocnv  7318  isotr  7324  isopolem  7333  isosolem  7335  f1oiso  7339  f1oiso2  7340  caovordig  7605  caovordg  7607  caovord  7611  caofrss  7703  caoftrn  7705  fr3nr  7759  dfwe2  7761  f1oweALT  7957  frxp  8110  poxp  8112  poxp2  8127  frxp2  8128  poxp3  8134  frxp3  8135  poseq  8142  suppimacnv  8158  tposoprab  8246  ertr  8698  ecopovsym  8805  ecopovtrn  8806  domeng  8947  eqeng  8971  en0r  9005  0fi  9027  snfi  9028  sbth  9073  domunsn  9103  domssex  9114  findcard  9136  findcard2  9137  nnfi  9140  pssnn  9141  unfi  9143  sbthfi  9171  nneneq  9178  onfin  9187  0sdom1dom  9194  1sdom2dom  9202  unxpdom  9207  isinf  9213  fineqvlem  9214  dif1ennnALT  9225  findcard3  9231  frfi  9233  fisupg  9236  nnsdomg  9247  prfi  9271  fiint  9274  mapfien2  9357  supmo  9400  eqsup  9404  supub  9407  suplub  9408  suplub2  9409  sup0  9415  supmax  9416  fisup2g  9417  fisupcl  9418  suppr  9420  supisolem  9422  supisoex  9423  infmo  9445  infpr  9453  ordtypecbv  9467  ordtypelem3  9470  ordtypelem6  9473  ordtypelem7  9474  ordtypelem9  9476  wemaplem1  9496  wemaplem2  9497  harval  9510  wemapwe  9654  ttrclss  9677  ttrclselem2  9683  r111  9735  cardf2  9917  isnum2  9919  cardval3  9926  cardnueq0  9938  carden2a  9940  cardlim  9946  isinffi  9966  onsdom  9970  harval2  9971  cardmin2  9973  ondomen  10009  alephnbtwn  10043  alephinit  10067  aceq3lem  10092  infmap2  10188  cfslb2n  10240  sornom  10249  isfin4  10269  fin23lem26  10297  fin23lem27  10300  fin1a2lem11  10382  fin1a2lem12  10383  hsmex  10404  domtriomlem  10414  dominf  10417  zorn2lem2  10469  zorn2lem7  10474  zorn2g  10475  axdclem  10491  axdc  10493  brdom7disj  10503  brdom6disj  10504  cardmin  10536  ficard  10537  alephval2  10545  dominfac  10546  cfpwsdom  10557  gchi  10597  fpwwe2lem11  10614  fpwwe2lem12  10615  canthp1lem1  10625  canthp1lem2  10626  pwfseqlem4a  10634  pwfseqlem4  10635  elina  10660  winainflem  10666  eltskg  10723  rankcf  10750  indpi  10880  nqereu  10902  nsmallnq  10950  ltbtwnnq  10951  ltrnq  10952  prcdnq  10966  genpcd  10979  genpnmax  10980  ltaddpr2  11008  ltexprlem4  11012  prlem936  11020  reclem2pr  11021  reclem3pr  11022  supexpr  11027  ltsosr  11067  ltasr  11073  recexsrlem  11076  mulgt0sr  11078  map2psrpr  11083  supsrlem  11084  axpre-lttri  11138  axpre-lttrn  11139  axpre-ltadd  11140  axpre-mulgt0  11141  axpre-sup  11142  ltletr  11290  letr  11292  ltne  11295  eqle  11300  dedekind  11361  dedekindle  11362  ltordlem  11727  elimgt0  12044  elimge0  12045  squeeze0  12109  lbreu  12156  lble  12158  sup2  12162  infm3  12165  suprlub  12170  supmul1  12175  supmullem1  12176  supmul  12178  infregelb  12190  nn2ge  12254  nnge1  12255  nnne0  12261  nnsub  12271  nominpos  12472  nnunb  12491  elnnnn0b  12539  nn0sub  12545  nn0ge2m1nn  12565  peano2uz2  12675  peano5uzi  12676  dfuzi  12678  uzind  12679  uzind3  12681  eluz1  12857  uzind4  12921  uzwo  12926  nnwof  12929  indstr2  12942  ublbneg  12948  zsupss  12952  uzsupss  12955  uzwo3  12958  zmin  12959  zmax  12960  zbtwnre  12961  rebtwnz  12962  elpq  12990  elpqb  12991  rpnnen1lem1  12993  rpnnen1lem3  12994  rpnnen1lem4  12995  rpnnen1lem5  12996  rpnnen1  12998  elrp  13009  mnfltxr  13143  xnn0n0n1ge2b  13148  xnn0ge0  13150  xrltnsym  13153  xrlttri  13155  xrlttr  13156  xrltletr  13173  xrletr  13174  ngtmnft  13183  xrltmin  13199  xrlemin  13201  ifle  13214  z2ge  13215  qbtwnre  13216  qbtwnxr  13217  qextlt  13220  qextle  13221  xltnegi  13233  xmullem2  13282  xmulasslem2  13299  xmulasslem  13302  xlemul1a  13305  xrsupexmnf  13322  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  supxrpnf  13335  supxrunb1  13336  supxrunb2  13337  reltxrnmnf  13360  infmremnf  13361  infmrp1  13362  ixxval  13371  elixx1  13372  elioo2  13404  iccid  13408  icc0  13411  repos  13464  fzval  13528  elfz1  13531  fzm1  13626  flval  13818  flval2  13838  dfceil2  13863  uzsup  13887  modid2  13922  modmuladdnn0  13942  addmodlteq  13973  ssnn0fi  14012  rabssnn0fi  14013  suppssfz  14021  serge0  14083  expge0  14125  expge1  14126  facdiv  14314  facwordi  14316  hashkf  14359  hashnnn0genn0  14370  hashv01gt1  14372  hashneq0  14391  hashdom  14406  hashnn0n0nn  14418  hashss  14436  hashgt12el  14449  hashgt12el2  14450  ishashinf  14490  hashge2el2dif  14507  hashge2el2difr  14508  fi1uzind  14534  wrdlen1  14581  fstwrdne0  14583  wrdl1exs1  14641  pfxsuffeqwrdeq  14725  pfxsuff1eqwrdeq  14726  ccats1pfxeq  14741  ccats1pfxeqrex  14742  pfxccatin12lem3  14759  wrdl2exs2  14973  2swrd2eqwrdeq  14980  rtrclreclem3  15087  relexpindlem  15090  relexpind  15091  shftfib  15099  shftfn  15100  2shfti  15107  resqrex  15291  cau3lem  15396  caubnd2  15399  sqreu  15402  limsuple  15519  limsupval2  15521  rlim2  15537  climi  15551  rlimi  15554  ello12r  15558  ello1mpt  15562  ello1d  15564  elo12r  15569  o1lo1  15578  rlimclim1  15586  rlimdm  15592  climeu  15596  climmo  15598  2clim  15613  o1co  15627  o1compt  15628  addcn2  15635  mulcn2  15637  reccn2  15638  cn1lem  15639  rlimo1  15658  lo1add  15668  lo1mul  15669  climsup  15711  caucvgrlem  15714  caucvgb  15721  summo  15758  zsum  15759  fsum  15761  o1fsum  15855  supcvg  15900  ntrivcvgn0  15942  ntrivcvgmullem  15945  prodmo  15980  zprod  15981  fprod  15985  fprodntriv  15986  rpnnen2lem4  16263  ruclem2  16278  sqrt2irr  16295  dvdsabsb  16323  0dvds  16324  dvdsle  16358  alzdvds  16368  dvdsext  16369  fzo0dvdseq  16371  2tp1odd  16400  2teven  16403  nn0onn  16428  divalglem10  16450  bitsinv1lem  16489  sadadd3  16509  bitsuz  16522  gcdval  16544  gcdcllem1  16547  gcdcllem2  16548  gcddvds  16551  bezoutlem4  16590  dvdsgcd  16592  dfgcd2  16594  dvdssq  16615  lcmcllem  16644  dvdslcm  16646  lcmledvds  16647  lcmgcdlem  16654  lcmdvds  16656  fissn0dvds  16667  dvdslcmf  16679  lcmfledvds  16680  lcmf  16681  lcmfunsnlem1  16685  lcmfunsnlem2lem1  16686  lcmfdvds  16690  coprmgcdb  16697  coprmdvds2  16702  cncongr1  16715  cncongr2  16716  isprm  16721  dvdsnprmd  16738  dvdsprm  16752  exprmfct  16753  isprm6  16763  prmexpb  16768  prmfac1  16769  rpexp  16771  nnoddn2prmb  16863  iserodd  16885  pceu  16896  pczpre  16897  pcdiv  16902  pcdvdsb  16919  difsqpwdvds  16937  pcmpt  16942  pcmptdvds  16944  oddprmdvds  16953  prmpwdvds  16954  unbenlem  16958  infpnlem2  16961  infpn2  16963  prmreclem1  16966  prmreclem2  16967  prmreclem3  16968  prmreclem5  16970  prmreclem6  16971  vdwlem9  17039  vdwlem10  17040  vdwlem13  17043  prmolefac  17096  prmgaplem4  17104  prmgaplem6  17106  setsstruct2  17224  setsexstruct2  17225  imasleval  17585  mreexexlem3d  17692  mreexexlem4d  17693  mreexexd  17694  prslem  18343  drsdirfi  18351  posi  18363  posasymb  18365  pospropd  18371  pleval2  18381  plttr  18386  pltletr  18387  pospo  18389  lubprop  18402  lublecllem  18404  glbprop  18415  glble  18416  joinlem  18427  joinle  18430  meetval2lem  18438  meetlem  18441  poslubmo  18455  posglbmo  18456  poslubd  18457  tleile  18465  isglbd  18555  lubl  18558  lubun  18561  tsrlin  18631  tsrlemax  18632  letsr  18639  smndex2dlinvh  18969  eqgen  19240  odeq  19611  odmulg  19617  sylow2alem2  19679  sylow2blem3  19683  efgval2  19785  efgsfo  19800  efgred  19809  efgredeu  19813  efgcpbllemb  19816  cyggex2  19958  gsummptnn0fz  20047  gsummptnn0fzfv  20048  pgpfaclem1  20144  pgpfaclem2  20145  pgpfaclem3  20146  ablfaclem2  20149  ablfaclem3  20150  omndadd  20189  0ringnnzr  20600  orngmul  20937  lidldvgen  21462  zndvds  21659  znleval  21664  islinds  21919  psrass1lem  22043  psrmulval  22054  mplmonmul  22147  opsrtoslem2  22167  mhpmulcl  22272  psdmul  22289  coe1mul2  22390  coe1tmmul2fv  22399  coe1pwmulfv  22401  gsummoncoe1  22429  pmatcoe1fsupp  22819  mp2pm2mplem4  22927  fvmptnn04ifa  22968  fvmptnn04ifd  22971  chfacffsupp  22974  chfacfscmul0  22976  chfacfpmmul0  22980  cpmadumatpoly  23001  cayleyhamilton  23008  cayleyhamiltonALT  23009  ordtbaslem  23306  ordtbas2  23309  ordtopn1  23312  mnfnei  23339  ordtt1  23497  ordthauslem  23501  ordthmeolem  23919  trust  24347  ucncn  24402  imasdsf1olem  24491  comet  24631  stdbdxmet  24633  stdbdmet  24634  stdbdmopn  24636  metcnpi  24662  metcnpi2  24663  metcnpi3  24664  ngptgp  24754  nlmvscnlem1  24804  nrginvrcnlem  24809  nmogelb  24834  nmolb  24835  nghmcn  24863  xrsxmet  24928  icccmplem2  24942  xrge0tsms  24953  xmetdcn2  24956  metdsf  24967  metdsge  24968  metdscn  24975  metnrmlem1a  24977  addcnlem  24983  cncfi  25014  elcncf1di  25015  iccpnfhmeo  25065  xrhmeo  25066  evth  25079  ipcnlem1  25365  lmmcvg  25381  cfili  25388  minveclem1  25544  minveclem3b  25548  minveclem6  25554  pmltpclem1  25568  pmltpc  25570  ivthlem2  25572  ovolmge0  25597  ovolgelb  25600  ovolctb  25610  ovoliun  25625  ovolshftlem1  25629  ovolscalem1  25633  ovolicc2lem3  25639  ovolicc2lem5  25641  ovolicc2  25642  voliunlem3  25672  ioombl1lem1  25678  ioombl1lem4  25681  volcn  25726  ismbfd  25759  mbfsup  25784  mbfinf  25785  mbflimsup  25786  itg1ge0  25806  mbfi1fseqlem5  25839  itg2val  25848  itg2const  25860  itg2const2  25861  itg2seq  25862  itg2monolem1  25870  itg2addlem  25878  itg2cnlem1  25881  itg2cnlem2  25882  itg2cn  25883  isibl  25885  ditgeq2  25969  dvferm1lem  26104  rolle  26110  c1lip1  26117  lhop1  26134  dvfsumlem2  26147  dvfsumlem4  26149  dvfsumrlim  26151  dvfsum2  26154  mdegmullem  26196  deg1leb  26213  deg1lt  26215  dvdsq1p  26281  dgrco  26393  plydivex  26419  quotcan  26431  aannenlem1  26450  aannenlem2  26451  ulmi  26507  ulmcaulem  26515  ulmcau  26516  ulmbdd  26519  ulmdvlem3  26523  psercnlem1  26546  psercn  26547  abelthlem8  26560  sinhalfpilem  26586  logltb  26723  cxple2  26820  cxpcn3lem  26870  isosctrlem1  26941  leibpilem2  27064  cxploglim  27100  scvxcvx  27108  lgamgulmlem4  27154  lgamgulmlem5  27155  vmaval  27235  isppw2  27237  muval  27254  fsumdvdscom  27307  dvdsflf1o  27309  dvdsflsumcom  27310  musum  27313  muinv  27315  ppiublem1  27324  chtub  27334  logfac2  27339  bpos1lem  27404  bposlem9  27414  lgsdir  27454  lgsne0  27457  lgsqr  27473  gausslemma2dlem0i  27486  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  2lgslem2  27517  2lgs  27529  2sqlem6  27545  2sqlem8  27548  2sqlem10  27550  2sq2  27555  2sqreulem1  27568  2sqreunnlem1  27571  dchrisumlema  27610  dchrisumlem2  27612  dchrisumlem3  27613  dchrvmasumiflem1  27623  dchrisum0fval  27627  dchrisum0ff  27629  dchrisum0flblem2  27631  logsqvma2  27665  pntrsumbnd2  27689  pntrlog2bndlem1  27699  pntpbnd1  27708  pntpbnd2  27709  pntibndlem2  27713  pntibndlem3  27714  pntibnd  27715  pntlemi  27726  pntlem3  27731  pntlemp  27732  pntleml  27733  pnt3  27734  nodenselem4  27809  nodenselem5  27810  nodenselem7  27812  nodense  27814  nolt02o  27817  nosupprefixmo  27822  noinfprefixmo  27823  nosupcbv  27824  nosupdm  27826  nosupfv  27828  nosupres  27829  nosupbnd1lem1  27830  nosupbnd1lem3  27832  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd1  27836  nosupbnd2lem1  27837  noinfcbv  27839  noinfdm  27841  noinfres  27844  noinfbnd1lem1  27845  noinfbnd1lem4  27848  noinfbnd1  27851  noinfbnd2lem1  27852  noinfbnd2  27853  noetalem2  27864  ltsne  27896  nocvxminlem  27905  sltssnb  27920  sltssepc  27922  conway  27930  cutsval  27931  etaslts  27944  lesrec  27950  eqcuts3  27955  0lt1s  27963  bday1  27965  cuteq1  27968  leftval  28000  elright  28003  sltsleft  28011  made0  28014  madecut  28034  right1s  28047  madebdaylemlrcut  28050  cofslts  28069  coinitslts  28070  cofcutr  28075  cofcutrtime  28078  cofss  28081  coiniss  28082  cutlt  28083  cutmax  28085  cutmin  28086  cutminmax  28087  addsproplem1  28120  addsprop  28127  leadds1  28140  addsuniflem  28152  negsproplem1  28179  negsprop  28186  negsid  28192  negsunif  28206  mulsproplemcbv  28266  mulsproplem1  28267  mulsproplem9  28275  mulsprop  28281  sltmuls1  28298  sltmuls2  28299  mulsuniflem  28300  precsexlemcbv  28357  precsexlem8  28365  precsexlem9  28366  precsexlem11  28368  precsex  28369  abssval  28390  oncutlt  28415  oniso  28422  bdayons  28427  n0sge0  28489  nnsge1  28494  n0fincut  28506  n0subs  28514  bdayn0p1  28520  eln0zs  28551  peano5uzs  28555  uzsind  28556  zcuts  28558  twocut  28574  expsval  28576  halfcut  28609  addhalfcut  28610  bdayfinbndcbv  28617  bdayfinbndlem1  28618  bdayfinbndlem2  28619  bdayfinbnd  28620  elreno  28642  elreno2  28646  0reno  28647  1reno  28648  readdscl  28650  remulscllem2  28652  tgjustc1  28702  tgjustc2  28703  tgldimor  28729  iscgrglt  28741  tgcgr4  28758  lnopp2hpgb  28994  axcontlem10  29232  umgrislfupgr  29382  lfgrnloop  29384  usgrislfuspgr  29446  fusgrmaxsize  29723  0vtxrusgr  29836  iswspthn  30107  wspthnon  30116  wwlksn0s  30119  wwlksnred  30150  wwlksnextwrd  30155  wwlksnextfun  30156  wwlksnextinj  30157  wwlksnextproplem1  30167  wwlksnextproplem2  30168  wwlksnextproplem3  30169  elwwlks2on  30219  elwspths2spth  30228  rusgrnumwwlks  30235  clwlkclwwlklem2  30260  clwlkclwwlkf1lem2  30265  clwwlkn0  30288  clwwlkinwwlk  30300  clwwlkf1  30309  clwwlkext2edg  30316  wwlksext2clwwlk  30317  clwlknf1oclwwlknlem2  30342  clwlknf1oclwwlknlem3  30343  clwlknf1oclwwlkn  30344  clwwlknonccat  30356  clwwlknonex2  30369  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  konigsberg  30517  frgrwopreglem2  30573  numclwwlk2lem1lem  30602  numclwwlk1lem2f1  30617  friendshipgt3  30658  vacn  30955  nmcvcn  30956  smcnlem  30958  nmobndi  31036  blocni  31066  ubthlem1  31131  ubthlem2  31132  ubthlem3  31133  minvecolem1  31135  minvecolem5  31142  minvecolem6  31143  norm3lemt  31413  hcaucvg  31447  hlimconvi  31452  hlim2  31453  chlimi  31495  hlimreui  31500  occl  31565  cmbr3  31869  cmcm  31875  cmcm3  31876  lecm  31878  cnopc  32174  cnfnc  32191  0cnop  32240  0cnfn  32241  idcnop  32242  nmopun  32275  nmcexi  32287  lnconi  32294  branmfn  32366  opsqrlem1  32401  pjnmopi  32409  pjnormssi  32429  stge1i  32499  strlem5  32516  hstrlem5  32524  mddmd2  32570  csmdsymi  32595  cvmd  32597  ela  32600  cvbr4i  32628  chirredlem3  32653  chirredlem4  32654  chirred  32656  atmd  32660  mdsym  32673  mddmdin0i  32692  cdj1i  32694  cdj3i  32702  fmptcof2  32914  isoun  32959  xrge0infss  33017  xnn0gt0  33026  sgnmulsgp  33089  toslublem  33205  tosglblem  33207  ismntd  33217  mgcmnt2  33226  dfmgc2lem  33228  dfmgc2  33229  xrge0tsmsd  33306  psgnfzto1st  33338  sgnsval  33394  xrnarchi  33417  archirng  33421  archiexdiv  33423  archiabllem1a  33424  archiabllem2a  33427  archiabl  33431  isarchiofld  33432  ellpi  33602  rprmdvds  33726  selvply1rhmlemb  33826  psrmonmul  33857  smatfval  34102  crefi  34154  pcmplfin  34167  ordtconnlem1  34231  qqhcn  34298  qqhucn  34299  esumcst  34370  esumpinfval  34380  esumpcvgval  34385  esumcvg  34393  esum2d  34400  oddpwdc  34661  eulerpartlems  34667  eulerpartlemf  34677  eulerpartlemt  34678  eulerpartlemr  34681  eulerpartlemgvv  34683  eulerpartlemn  34688  dstfrvunirn  34782  ballotlemfcc  34801  signslema  34866  hgt749d  34953  bnj1185  35098  bnj602  35220  bnj1228  35316  fnrelpredd  35397  nummin  35399  fineqvnttrclse  35432  onvfowev  35471  loop1cycl  35500  umgr2cycllem  35503  acycgrcycl  35510  acycgr1v  35512  subfacp1lem1  35542  fundmpss  36130  funbreq  36133  wsuclb  36189  brtxp  36241  brtxp2  36242  brpprod3a  36247  elfix  36264  sscoid  36274  elfuns  36276  fnsingle  36280  brimageg  36288  fnimage  36290  brdomaing  36296  brrangeg  36297  funpartlem  36305  dfrecs2  36313  fvtransport  36395  trer  36689  elicc3  36690  finminlem  36691  nn0prpwlem  36695  nn0prpw  36696  fnessref  36730  refssfne  36731  fnemeet2  36740  filnetlem3  36753  weiunlem  36836  weiunfrlem  36837  dnicn  36943  unblimceq0  36958  knoppndvlem21  36983  bj-seex  37419  dfgcd3  37828  icorempo  37857  icoreval  37859  relowlssretop  37869  phpreu  38115  fin2so  38118  poimirlem14  38145  poimirlem15  38146  poimirlem23  38154  poimirlem28  38159  poimirlem31  38162  heicant  38166  mblfinlem1  38168  mblfinlem2  38169  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  itg2addnclem  38182  itg2addnc  38185  itg2gt0cn  38186  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  frinfm  38246  fdc1  38257  nninfnub  38262  equivbnd  38301  heibor1lem  38320  heiborlem8  38329  iccbnd  38351  inxprnres  38809  ref5  38830  brxrn  38894  brxrn2  38895  dfxrn2  38896  xrninxp  38926  brcoss  39032  cossssid4  39071  eqvreltr  39202  oposlem  39818  lub0N  39825  glb0N  39829  omllaw  39879  cvrval  39905  cvrnbtwn  39907  cvrnbtwn2  39911  cvrnbtwn3  39912  cvrcon3b  39913  cvrnbtwn4  39915  cvrcmp  39919  isat  39922  atnlt  39949  atlex  39952  cvlexch1  39964  cvlexchb1  39966  cvlatexch1  39972  glbconN  40013  2llnne2N  40044  cvratlem  40057  cvrat4  40079  ps-1  40113  3at  40126  islln  40142  llncmp  40158  llnnlt  40159  islpln  40166  islpln5  40171  lvolex3N  40174  lplncmp  40198  lplnexllnN  40200  lplnnlt  40201  islvol  40209  lvoli3  40213  islvol5  40215  lvolcmp  40253  lvolnltN  40254  dalem-cly  40307  dalem44  40352  pmapval  40393  pmapglbx  40405  lncvrelatN  40417  lncmp  40419  cdlemblem  40429  llnexchb2  40505  lautle  40720  lautcvr  40728  ldilset  40745  ltrnset  40754  trlset  40797  cdlemc4  40830  cdleme11dN  40898  cdleme20k  40955  cdleme21ct  40965  cdleme22b  40977  tendoex  41611  diafval  41667  diaval  41668  dicfval  41811  dihfval  41867  dihglblem2N  41930  lcmineqlem23  42680  primrootlekpowne0  42734  hashnexinjle  42758  sticksstones1  42775  sticksstones2  42776  sticksstones10  42784  sticksstones12a  42786  sticksstones22  42797  rhmqusspan  42814  qsalrel  42869  supinf  42870  dvdsexpnn0  42955  sn-nnne0  43094  sn-sup2  43125  fimgmcyclem  43163  prjspner1  43220  flt4lem7  43253  nna4b4nsq  43254  lzenom  43363  fphpdo  43406  rencldnfilem  43409  irrapxlem5  43415  irrapxlem6  43416  pellexlem3  43420  pellqrex  43468  pellfundre  43470  pellfundge  43471  pellfundlb  43473  pellfundglb  43474  monotoddzz  43532  oddcomabszz  43533  zindbi  43535  jm2.22  43584  jm2.23  43585  rpnnen3  43621  ttac  43625  fnwe2lem2  43640  aomclem8  43650  hbtlem1  43712  hbtlem5  43717  safesnsupfidom1o  44005  safesnsupfilb  44006  harval3  44126  undmrnresiss  44192  refimssco  44195  rfovcnvf1od  44592  fsovrfovd  44597  cpcolld  44832  cpcoll2d  44833  grucollcld  44834  nzss  44891  relprel  45525  permaxrep  45580  permaxsep  45581  permaxnul  45582  permaxpow  45583  permaxpr  45584  permaxun  45585  permaxinf2lem  45586  permac8prim  45588  nregmodel  45591  uzwo4  45631  wessf1ornlem  45761  dmrelrnrel  45800  rnmptbdd  45818  rnmptbd2lem  45821  rnmptbd2  45822  rnmptbd  45829  xreqle  45894  infxr  45940  infleinf  45945  unb2ltle  45987  rexabsle  45991  uzublem  46002  uzub  46003  infxrgelbrnmpt  46026  cvgcau  46062  rexanuz2nf  46064  climinf  46180  limsupre  46213  addlimc  46220  0ellimcdiv  46221  limclner  46223  climd  46244  clim2d  46245  limsupref  46257  limsupbnd1f  46258  limsuppnfdlem  46273  limsuppnfd  46274  limsuppnf  46283  limsupubuzlem  46284  limsupubuz  46285  limsupubuzmpt  46291  limsupmnf  46293  limsupre2  46297  limsupmnfuz  46299  limsupre2mpt  46302  limsupre3lem  46304  limsupre3  46305  limsupre3mpt  46306  limsupre3uz  46308  limsupreuz  46309  limsupreuzmpt  46311  climuz  46316  climisp  46318  climrescn  46320  climxrrelem  46321  climxrre  46322  liminflelimsuplem  46347  liminfreuzlem  46374  liminfreuz  46375  xlimpnfxnegmnf  46386  xlimmnfv  46406  xlimmnf  46413  xlimmnfmpt  46415  dfxlim2  46420  dvbdfbdioo  46502  ioodvbdlimc1lem1  46503  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvnxpaek  46514  stoweidlem14  46586  stoweidlem29  46601  stoweidlem31  46603  stoweidlem34  46606  stoweidlem49  46621  wallispilem3  46639  stirlinglem13  46658  stirlinglem14  46659  fourierdlem16  46695  fourierdlem20  46699  fourierdlem21  46700  fourierdlem22  46701  fourierdlem25  46704  fourierdlem39  46718  fourierdlem41  46720  fourierdlem42  46721  fourierdlem51  46729  fourierdlem54  46732  fourierdlem64  46742  fourierdlem77  46755  fourierdlem83  46761  fourierdlem87  46765  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  fouriersw  46803  etransclem48  46854  sge0seq  47018  sge0reuz  47019  meaiunincf  47055  hsphoif  47148  hsphoival  47151  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmv1lelem3  47165  hoidmv1le  47166  hoidmvlelem2  47168  hoidmvlelem5  47171  hspmbllem2  47199  salpreimalegt  47281  pimdecfgtioc  47287  pimincfltioo  47290  salpreimaltle  47298  issmf  47300  smfpreimalt  47303  smfpreimaltf  47308  incsmf  47314  issmfle  47317  smfpimltxr  47319  smfpreimale  47326  decsmf  47339  smfrec  47361  smfsup  47386  fsupdm  47414  et-sqrtnegnre  47445  ormklocald  47448  natlocalincr  47450  rlimdmafv  47769  funressndmafv2rn  47815  tz6.12c-afv2  47834  tz6.12i-afv2  47835  funressnbrafv2  47836  dfatbrafv2b  47837  funbrafv2  47839  fnbrafv2b  47840  dfatcolem  47847  rlimdmafv2  47850  nnmul2  47922  2ltceilhalf  47924  zplusmodne  47941  m1modne  47946  minusmod5ne  47947  submodneaddmod  47949  modmknepk  47960  iccpartiltu  48026  iccpartgt  48031  icceuelpartlem  48039  iccpartnel  48042  sprsymrelfolem2  48097  nprmmul2  48132  prmdvdsfmtnof1  48194  sfprmdvdsmersenne  48210  lighneallem3  48214  lighneallem4a  48215  lighneallem4b  48216  lighneallem4  48217  proththdlem  48220  nprmdvdsfacm1lem2  48228  iseven2  48271  isodd3  48272  gbegt5  48381  gbowgt5  48382  gboge9  48384  sbgoldbwt  48397  sbgoldbst  48398  sbgoldbaltlem1  48399  sgoldbeven3prm  48403  sbgoldbm  48404  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  evengpop3  48418  evengpoap3  48419  bgoldbnnsum3prm  48424  bgoldbtbndlem4  48428  bgoldbtbnd  48429  bgoldbachlt  48433  tgblthelfgott  48435  tgoldbachlt  48436  tgoldbach  48437  cycl3grtri  48567  assintopval  48825  ply1mulgsumlem2  49018  ldepsnlinc  49139  dig1  49239  rrxsphere  49379  xpco2  49486  lubsscl  49589  glbsscl  49590  ipolub  49617  ipoglb  49620  catprslem  49639  uobffth  49847  uobeqw  49848