Theorem breq1 5089

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

Assertion

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

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 4817	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2822	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 5087	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 5087	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breq12  5091  breq1i  5093  breq1d  5096  nbrne2  5106  brab1  5134  pocl  5538  swopolem  5540  swopo  5541  po2ne  5546  solin  5557  sotrieq  5561  sotr2  5564  isso2i  5567  somo  5569  dffr2  5583  frc  5585  frirr  5598  fr2nr  5599  wereu2  5619  vtoclr  5685  frsn  5710  brcog  5813  brcogw  5815  brcnvg  5826  dfdmf  5843  eldmg  5845  dmun  5857  dm0rn0  5871  dfrnf  5897  dmcosseq  5925  dmcosseqOLD  5926  dfres2  5998  imasng  6041  cotrg  6066  cnvsym  6069  asymref2  6072  sotri2  6084  somin1  6088  rnco  6208  coi1  6219  predtrss  6278  frpomin  6296  dffun2  6500  dffun6f  6505  funmo  6506  fun11  6564  fveq2  6832  eliman0  6869  nfunsn  6871  dffv2  6927  fvopab5  6973  dff3  7044  f1ompt  7055  fmptco  7074  dff13  7200  foeqcnvco  7246  isorel  7272  soisores  7273  soisoi  7274  isocnv  7276  isotr  7282  isomin  7283  isoini  7284  isopolem  7291  isosolem  7293  f1oiso  7297  f1oiso2  7298  weniso  7300  eqfunresadj  7306  caovordig  7563  caovordg  7565  caovord3d  7568  caovord  7569  caovord3  7571  caofrss  7661  caoftrn  7663  fr3nr  7717  dfwe2  7719  f1oweALT  7916  frxp  8067  poxp  8069  fnse  8074  poxp2  8084  frxp2  8085  poxp3  8091  frxp3  8092  xpord3pred  8093  poseq  8099  brtpos2  8173  rntpos  8180  tpostpos  8187  frrlem12  8238  ertr  8650  ecopovsym  8757  ecopovtrn  8758  isfi  8913  en0  8956  en0ALT  8957  en1  8962  endisj  8993  xpcomco  8996  sbth  9026  2pwne  9062  disjenex  9064  ssenen  9080  findcard  9089  findcard2  9090  pssnn  9094  sbthfi  9124  nneneq  9131  php  9132  onomeneq  9139  sdom1  9151  1sdom2dom  9155  isinf  9166  fineqvlem  9167  en1eqsnbi  9177  findcard3  9184  frfi  9186  fiint  9228  mapfienlem1  9309  mapfienlem2  9310  mapfienlem3  9311  mapfien  9312  marypha1lem  9337  supmo  9356  eqsup  9360  supub  9363  suplub  9364  suppr  9376  supisolem  9378  supisoex  9379  infmin  9400  infmo  9401  fiinfg  9405  fiinf2g  9406  infpr  9409  ordtypecbv  9423  ordtypelem3  9426  ordtypelem6  9429  ordtypelem7  9430  ordtypelem9  9432  ordtypelem10  9433  hartogslem1  9448  hartogs  9450  wemaplem1  9452  wemaplem2  9453  wemapso2lem  9458  card2on  9460  card2inf  9461  elharval  9467  brwdom2  9479  wdomtr  9481  cantnfs  9576  cantnfp1lem2  9589  oemapso  9592  cantnflem1  9599  wemapwe  9607  ttrclss  9630  r111  9688  kardex  9807  karden  9808  isnumi  9859  tskwe  9863  cardid2  9866  cardonle  9870  cardne  9878  iscard2  9889  infxpenlem  9924  fodomfi2  9971  wdomfil  9972  wdomnumr  9975  alephsuc2  9991  infenaleph  10002  iunfictbso  10025  infpss  10127  cff1  10169  cfslb2n  10179  sornom  10188  fin4i  10209  isfin6  10211  isfin7  10212  isfin1-3  10297  fin1a2lem9  10319  fin1a2lem11  10321  hsmexlem4  10340  axcc2lem  10347  axcc4dom  10352  domtriomlem  10353  numthcor  10405  zorn2lem2  10408  zorn2lem3  10409  zorn2lem7  10413  zorn2g  10414  axdclem  10430  axdc  10432  brdom7disj  10442  brdom6disj  10443  uniimadom  10455  ondomon  10474  alephval2  10484  alephreg  10494  pwcfsdom  10495  elgch  10534  gchi  10536  fpwwe2lem11  10553  fpwwe2lem12  10554  winainflem  10605  winalim2  10608  tsken  10666  0tsk  10667  inar1  10687  tskord  10692  tskuni  10695  grudomon  10729  pinq  10839  nqereu  10841  enqeq  10846  ltbtwnnq  10890  ltrnq  10891  prcdnq  10905  prnmax  10907  genpnmax  10919  nqpr  10926  1idpr  10941  reclem2pr  10960  reclem3pr  10961  reclem4pr  10962  recexpr  10963  supexpr  10966  ltsosr  11006  1ne0sr  11008  ltasr  11012  supsrlem  11023  axpre-lttri  11077  axpre-lttrn  11078  axpre-ltadd  11079  axpre-sup  11081  lelttr  11225  dedekind  11298  dedekindle  11299  ltordlem  11664  lt0ne0d  11704  fimaxre3  12091  fiminre2  12093  lbreu  12095  lble  12097  sup2  12101  infm3  12104  suprleub  12111  supaddc  12112  supadd  12113  supmul1  12114  supmullem1  12115  supmul  12117  nnne0  12200  nnsub  12210  nominpos  12403  nnunb  12422  arch  12423  nn0sub  12476  nn0n0n1ge2b  12495  nn0lt10b  12580  zextle  12591  peano5uzti  12608  fzind  12616  btwnz  12621  uzval  12779  uzwo  12850  nnwof  12853  ublbneg  12872  lbzbi  12875  zsupss  12876  uzsupss  12879  uzwo3  12882  zmax  12884  rebtwnz  12886  rpnnen1lem3  12918  xrltnsym  13077  xrlttri  13079  xrlttr  13080  xrlelttr  13096  nltpnft  13105  xrmaxlt  13122  xrmaxle  13124  qbtwnre  13140  qbtwnxr  13141  xltnegi  13157  xnn0lenn0nn0  13186  xsubge0  13202  xlesubadd  13204  xmullem2  13206  xlemul1a  13229  xrinfmexpnf  13247  xrsupsslem  13248  xrinfmsslem  13249  xrub  13253  supxrunb1  13260  supxrunb2  13261  reltre  13282  rpltrp  13283  reltxrnmnf  13284  ixxval  13295  elixx1  13296  elioo2  13328  iccid  13332  icc0  13335  fzval  13452  elfz1  13455  elfznelfzo  13717  elfznelfzob  13718  flval  13742  fllelt  13745  flflp1  13755  flval2  13762  flval3  13763  flbi  13764  dfceil2  13787  ceilval2  13788  fleqceilz  13802  modid2  13846  addmodlteq  13897  fsequb2  13927  ssnn0fi  13936  seqf1olem2  13993  sqlecan  14160  faclbnd4lem1  14244  hashsnle1  14368  pr2pwpr  14430  hash3tpde  14444  rtrclreclem3  15011  relexpindlem  15014  sgnval  15039  01sqrexlem6  15198  01sqrex  15200  abslt  15266  absle  15267  rexanre  15298  rexico  15305  limsupgle  15428  limsupgre  15432  limsupbnd2  15434  rlim2lt  15448  rlim3  15449  ello12r  15468  ello1d  15474  elo12r  15479  rlimconst  15495  climshft  15527  rlimcn3  15541  o1rlimmul  15570  lo1le  15603  climsup  15621  caucvgrlem  15624  isumless  15799  divrcnv  15806  cvgrat  15837  rpnnen2lem10  16179  ruclem1  16187  ruclem2  16188  ruclem11  16196  ruclem12  16197  sqrt2irr  16205  absdvdsb  16232  dvdsle  16268  dvdsabseq  16271  dvdsdivcl  16274  dvdsext  16279  divalglem8  16358  divalglem9  16359  divalglem10  16360  divalgmod  16364  ndvdssub  16367  sadcaddlem  16415  gcdcllem1  16457  gcdcllem2  16458  gcdcllem3  16459  dfgcd2  16504  gcdzeq  16510  dvdssq  16525  nn0seqcvgd  16528  algcvgblem  16535  lcmval  16550  lcmdvds  16566  lcmgcdeq  16570  lcmfpr  16585  lcmf  16591  lcmftp  16594  lcmfunsnlem1  16595  lcmfunsnlem2lem1  16596  lcmfunsnlem2lem2  16597  lcmfdvdsb  16601  coprmgcdb  16607  coprmdvds1  16610  1nprm  16637  1idssfct  16638  isprm2lem  16639  isprm2  16640  dvdsprime  16645  nprm  16646  3prm  16652  dvdsprm  16662  exprmfct  16663  isprm5  16666  maxprmfct  16668  coprm  16670  prmdvdsncoprmbd  16686  ncoprmlnprm  16687  eulerthlem2  16741  phisum  16750  odzval  16751  pythagtriplem4  16779  pc2dvds  16839  pcprmpw2  16842  pcprmpw  16843  dvdsprmpweqle  16846  oddprmdvds  16863  prmpwdvds  16864  pockthg  16866  unbenlem  16868  prmreclem4  16879  prmreclem5  16880  prmreclem6  16881  1arith  16887  vdwlem6  16946  vdwlem11  16951  vdwlem13  16953  ramtlecl  16960  ramub  16973  rami  16975  ramubcl  16978  0ram  16980  ram0  16982  prmdvdsprmop  17003  prmolefac  17006  prmodvdslcmf  17007  prmgaplem2  17010  prmgaplcmlem1  17011  prmgaplcmlem2  17012  prmgaplem3  17013  prmgaplem4  17014  prmgaplem5  17015  prmgaplem6  17016  prmgapprmolem  17021  prmlem0  17065  prmlem1a  17066  imasaddfnlem  17481  imasvscafn  17490  imasleval  17494  prslem  18252  drsdir  18257  drsdirfi  18260  isdrs2  18261  posi  18272  posasymb  18274  pospropd  18280  pltval3  18292  plelttr  18297  pospo  18298  lubprop  18311  luble  18312  lublecllem  18313  glbprop  18324  joinval2lem  18333  joinlem  18336  meetlem  18350  meetle  18353  poslubmo  18364  posglbmo  18365  poslubd  18366  tleile  18374  latnlej  18411  isglbd  18464  lubub  18466  lubun  18470  clatleglb  18473  tsrlin  18540  letsr  18548  dirge  18558  pmtrval  19415  pmtrrn  19421  pmtrfrn  19422  pmtrrn2  19424  pmtrsn  19483  mndodcongi  19507  odeq  19514  odmulgeq  19521  gexnnod  19552  sylow1lem1  19562  pgpssslw  19578  sylow2a  19583  efgredeu  19716  efgred2  19717  gexex  19817  frgpnabllem2  19838  cyggenod  19848  dprdval  19969  dprdw  19976  dprdwd  19977  ablfacrplem  20031  ablfac1c  20037  ablfac1eu  20039  ablfaclem3  20053  omndadd  20092  abvtrivd  20798  zringlpir  21455  prmirredlem  21460  znleval  21542  frlmelbas  21744  ellspd  21790  islindf4  21826  psrbagconcl  21915  psrbagleadd1  21916  gsumbagdiaglem  21918  rhmpsrlem2  21929  psrlidm  21949  psrridm  21950  psrass1  21951  psrcom  21955  mplelbas  21978  mplmonmul  22023  ltbwe  22031  mhpmulcl  22124  psdmul  22141  coe1fsupp  22187  coe1ae0  22189  coe1mul2  22243  coe1tmmul  22251  pmatcoe1fsupp  22675  chfacffsupp  22830  chfacfscmulfsupp  22833  chfacfscmulgsum  22834  chfacfpmmulfsupp  22837  chfacfpmmulgsum  22838  ordtbas2  23165  ordtopn2  23169  ordtrest2lem  23177  pnfnei  23194  ordtt1  23353  ordthauslem  23357  2ndci  23422  2ndcsb  23423  2ndcredom  23424  2ndc1stc  23425  1stcrest  23427  2ndcctbss  23429  2ndcdisj  23430  2ndcsep  23433  lly1stc  23470  tx1stc  23624  ordthmeolem  23775  ufildom1  23900  xmetrtri2  24330  prdsxmetlem  24342  ssblex  24402  prdsbl  24465  comet  24487  stdbdxmet  24489  stdbdmopn  24492  met1stc  24495  dscmet  24546  metdstri  24826  metdscn  24831  xrhmeo  24922  bndth  24934  evth  24935  lebnumlem3  24939  pcovalg  24988  pco1  24991  pcocn  24993  pcopt  24998  pcopt2  24999  pcoass  25000  nmoleub3  25095  bcthlem5  25304  rrxfsupp  25378  minveclem4c  25401  minveclem2  25402  minveclem3b  25404  minveclem4  25408  minveclem6  25410  pmltpclem1  25424  pmltpc  25426  ovollb2lem  25464  ovolctb  25466  ovolunlem1  25473  ovoliunlem1  25478  ovoliunlem2  25479  ovoliun2  25482  ovolshftlem1  25485  ovolscalem1  25489  ovolicc1  25492  ovolicc2lem3  25495  voliunlem2  25527  voliunlem3  25528  ioombl1lem4  25537  uniioovol  25555  uniioombllem2  25559  uniioombllem3  25561  uniioombllem6  25564  volsup2  25581  ismbfd  25615  mbfsup  25640  mbflimsup  25642  itg1climres  25690  mbfi1fseqlem4  25694  itg2lr  25706  itg2leub  25710  itg2seq  25718  itg2monolem1  25726  itg2monolem3  25728  itg2mono  25729  itg2i1fseq2  25732  itg2gt0  25736  itg2cnlem1  25737  itg2cnlem2  25738  itg2cn  25739  iblss  25781  itgless  25793  ibladdlem  25796  iblabsr  25806  iblmulc2  25807  itgabs  25811  bddiblnc  25818  ditgeq1  25824  dvferm2lem  25962  rolle  25966  dvlip2  25972  c1liplem1  25973  c1lip1  25974  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumlem4  26008  mdegleb  26041  degltlem1  26049  plyco0  26169  plyeq0lem  26187  coeeq2  26219  dgrle  26220  dgradd2  26245  plydiveu  26277  aareccl  26305  aalioulem2  26312  aaliou3lem7  26328  psercnlem1  26406  pilem2  26433  pilem3  26434  logltb  26580  divlogrlim  26615  logcnlem3  26624  cxpaddlelem  26732  rlimcnp  26946  cxplim  26953  cxploglim  26959  scvxcvx  26967  ftalem1  27054  ftalem2  27055  isppw2  27096  vmappw  27097  sgmnncl  27128  sqff1o  27163  fsumdvdsdiaglem  27164  dvdsppwf1o  27167  dvdsflsumcom  27169  musum  27172  muinv  27174  mpodvdsmulf1o  27175  dvdsmulf1o  27177  vmalelog  27187  vmasum  27198  logfac2  27199  perfectlem2  27212  bcmono  27259  bpos1lem  27264  bposlem9  27274  lgsmod  27305  lgsne0  27317  gausslemma2dlem4  27351  2sqlem6  27405  2sqlem8  27408  2sqlem10  27410  2sqreulem1  27428  2sqreunnlem1  27431  chtppilim  27457  rpvmasumlem  27469  dchrisumlema  27470  dchrisumlem2  27472  dchrvmasumlem1  27477  dchrvmasumiflem1  27483  dchrisum0flblem1  27490  dchrisum0flblem2  27491  dchrisum0  27502  rplogsum  27509  logsqvma  27524  pntpbnd1  27568  pntpbnd2  27569  pntibndlem3  27574  pntlemj  27585  pntlemi  27586  pntlem3  27591  pnt3  27594  ostth3  27620  nodense  27675  noresle  27680  nosupprefixmo  27683  noinfprefixmo  27684  nosupcbv  27685  nosupdm  27687  nosupbnd1lem1  27691  nosupbnd1lem4  27694  nosupbnd1  27697  nosupbnd2lem1  27698  nosupbnd2  27699  noinfcbv  27700  noinfdm  27702  noinffv  27704  noinfres  27705  noinfbnd1lem3  27708  noinfbnd1lem4  27709  noinfbnd1lem5  27710  noinfbnd1  27712  noetalem2  27725  nocvxminlem  27765  sltssnb  27780  sltssepc  27782  conway  27790  cutsval  27791  etaslts  27804  lesrec  27810  eqcuts3  27815  bday1  27825  cuteq1  27828  madeval2  27844  rightval  27861  elleft  27862  sltsright  27872  made0  27874  madecut  27894  left1s  27906  madebdaylemlrcut  27910  ltslpss  27919  cofslts  27929  coinitslts  27930  cofcutr  27935  cofcutrtime  27938  cofss  27941  coiniss  27942  cutmax  27945  cutmin  27946  cutminmax  27947  addsproplem1  27980  addsprop  27987  leadds1  28000  addsuniflem  28012  negsproplem1  28039  negsprop  28046  negsid  28052  negsunif  28066  mulsproplemcbv  28126  mulsproplem1  28127  mulsproplem9  28135  mulsprop  28141  sltmuls1  28158  sltmuls2  28159  mulsuniflem  28160  precsexlem11  28228  abslts  28260  oncutlt  28275  oniso  28282  bdayons  28287  addonbday  28290  n0fincut  28366  onsfi  28367  n0subs  28374  bdayn0p1  28380  eucliddivs  28387  zcuts  28418  twocut  28434  halfcut  28469  addhalfcut  28470  bdaypw2n0bndlem  28474  bdayfinbndcbv  28477  bdayfinbndlem1  28478  bdayfinbndlem2  28479  z12bdaylem1  28481  elreno  28502  elreno2  28506  tgjustc1  28562  tgjustc2  28563  iscgrglt  28601  tgcgr4  28618  hlcgreu  28705  lmif  28872  islmib  28874  trgcopyeu  28893  iscgrad  28898  inaghl  28932  axlowdim2  29048  axlowdim  29049  axcontlem2  29053  axcontlem3  29054  axcontlem4  29055  axcontlem7  29058  axcontlem9  29060  axcontlem10  29061  axcontlem11  29062  axcontlem12  29063  ebtwntg  29070  umgrupgr  29191  nbusgrvtxm1  29467  crctcshwlkn0lem2  29899  crctcshwlkn0lem3  29900  crctcsh  29912  wlkswwlksf1o  29967  clwlkclwwlklem2fv1  30085  clwlkclwwlkf  30098  0clwlkv  30221  eupth2  30329  numclwwlk5  30478  nmoubi  30863  minvecolem2  30966  minvecolem3  30967  minvecolem4c  30970  minvecolem4  30971  minvecolem5  30972  minvecolem6  30973  htthlem  31008  chlimi  31325  chcompl  31333  hsn0elch  31339  cmbr3  31699  cmcm  31705  cmcm3  31706  lecm  31708  nmopub  31999  nmfnleub  32016  nmopun  32105  nmcexi  32117  cnlnadjlem7  32164  pjnmopi  32239  stle0i  32330  stlesi  32332  stm1i  32334  csmdsymi  32425  cvmd  32427  atcveq0  32439  atcv1  32471  atord  32479  atcvat2  32480  chirred  32486  mdsym  32503  mddmdin0i  32522  cdj1i  32524  fmptcof2  32750  fnpreimac  32763  isoun  32795  fcobijfs  32814  fcobijfs2  32815  lt2addrd  32843  xlt2addrd  32852  xrge0infss  32853  infxrge0glb  32858  xrofsup  32860  fz1nnct  32894  sgnmulsgn  32935  toslublem  33052  tosglblem  33054  ismntd  33064  mgccole1  33070  mgccole2  33071  mgcmnt1  33072  mgcmnt2  33073  dfmgc2lem  33075  dfmgc2  33076  psgnfzto1stlem  33181  fzto1st  33184  psgnfzto1st  33186  trsp2cyc  33204  xrnarchi  33265  archirng  33269  archiexdiv  33271  archiabl  33279  isarchiofld  33280  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  elrgspn  33327  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  elrgspnsubrun  33330  linds2eq  33461  elrspunidl  33508  elrspunsn  33509  isrprm  33597  evl1deg1  33656  evl1deg2  33657  evl1deg3  33658  extvfvvcl  33699  extvfvcl  33700  mplmulmvr  33703  evlextv  33706  mplvrpmlem  33707  mplvrpmfgalem  33708  mplvrpmga  33709  mplvrpmmhm  33710  mplvrpmrhm  33711  psrmonmul  33714  psrmonprod  33716  esplyfval0  33728  esplylem  33730  esplyfv1  33733  esplyfval3  33736  esplyfvaln  33738  esplyind  33739  ply1degltdimlem  33787  lbsdiflsp0  33791  fedgmullem1  33794  fedgmullem2  33795  fedgmul  33796  fldextrspunlsplem  33838  fldextrspunlsp  33839  smatrcl  33961  smatlem  33962  madjusmdetlem2  33993  madjusmdet  33996  cmpcref  34015  ldlfcntref  34019  dispcmp  34024  zarcmplem  34046  ordtrest2NEWlem  34087  ordtconnlem1  34089  xrge0iifiso  34100  rge0scvg  34114  gsumesum  34224  esumfsup  34235  esumpinfval  34238  esumpcvgval  34243  esumcvg  34251  sigaclcu  34282  sigaclci  34297  unelsiga  34299  unelldsys  34323  sigapildsys  34327  ldgenpisyslem1  34328  fiunelros  34339  measvun  34374  voliune  34394  volfiniune  34395  oms0  34462  omssubaddlem  34464  omssubadd  34465  carsgsigalem  34480  carsgclctunlem2  34484  carsgclctun  34486  pmeasmono  34489  pmeasadd  34490  orvcval2  34624  dstfrvel  34639  ballotlemfc0  34658  ballotlemfcc  34659  ballotlemsv  34675  ballotlemsf1o  34679  breprexp  34798  tgoldbachgt  34828  bnj23  34882  bnj1185  34956  bnj1152  35161  bnj1418  35203  fnrelpredd  35255  loop1cycl  35340  umgr2cycl  35344  acycgrcycl  35350  dfdm5  35976  dfrn5  35977  wzel  36025  wsuclem  36026  brpprod  36086  brsset  36090  brbigcup  36099  dffix2  36106  elfuns  36116  brimageg  36128  brdomaing  36136  brrangeg  36137  brimg  36138  brapply  36139  lemsuccf  36142  funpartlem  36145  brrestrict  36152  dfrecs2  36153  dfrdg4  36154  brofs  36208  btwncomim  36216  btwnintr  36222  btwnexch3  36223  btwnexch2  36226  brifs  36246  brcolinear2  36261  colineardim1  36264  brfs  36282  btwnconn1  36304  segcon2  36308  seglerflx  36315  seglemin  36316  btwnsegle  36320  colinbtwnle  36321  broutsideof2  36325  fvray  36344  lineunray  36350  lineelsb2  36351  linerflx1  36352  trer  36519  elicc3  36520  finminlem  36521  nn0prpwlem  36525  nn0prpw  36526  fnessref  36560  refssfne  36561  weiunlem  36666  weiunfrlem  36667  weiunfr  36670  weiunse  36671  unblimceq0lem  36779  unblimceq0  36780  unbdqndv2  36784  knoppndvlem21  36805  taupilemrplb  37647  dfgcd3  37651  icorempo  37678  icoreval  37680  iooelexlt  37689  relowlssretop  37690  domalom  37731  ctbssinf  37733  pibt2  37744  phpreu  37936  fin2solem  37938  fin2so  37939  ltflcei  37940  ptrecube  37952  poimirlem1  37953  poimirlem2  37954  poimirlem5  37957  poimirlem6  37958  poimirlem7  37959  poimirlem9  37961  poimirlem12  37964  poimirlem22  37974  poimirlem23  37975  poimirlem24  37976  poimirlem26  37978  poimirlem27  37979  poimirlem32  37984  heicant  37987  mblfinlem1  37989  mblfinlem2  37990  itg2addnclem  38003  itg2addnclem3  38005  itg2addnc  38006  itg2gt0cn  38007  ibladdnclem  38008  iblmulc2nc  38017  itgabsnc  38021  ftc1anclem5  38029  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  indexdom  38066  filbcmb  38072  fdc  38077  prdsbnd  38125  heiborlem3  38145  rrnequiv  38167  rngoueqz  38272  eqbrtr  38570  elrnressn  38612  inxprnres  38630  presucmap  38827  eqvreltr  39023  prtlem10  39322  lsatcveq0  39489  lsatcv1  39505  oposlem  39639  opnlen0  39645  lub0N  39646  glb0N  39650  omllaw  39700  cmtbr4N  39712  cvrval  39726  cvrnbtwn  39728  cvrnbtwn2  39732  cvrnbtwn3  39733  cvrcon3b  39734  cvrnbtwn4  39736  atcvreq0  39771  atnle  39774  atlatmstc  39776  cvlexch1  39785  glbconN  39834  hlsuprexch  39838  exatleN  39861  cvratlem  39878  atcvrj0  39885  atcvrj2b  39889  atlelt  39895  cvrat4  39900  3dim1lem5  39923  3dim2  39925  3dim3  39926  ps-2  39935  llni  39965  llnn0  39973  llnle  39975  lplni  39989  lplni2  39994  lplnle  39997  lplnn0N  40004  llncvrlpln  40015  2llnjN  40024  lvoli  40032  lvoli3  40034  lvoli2  40038  lvoln0N  40048  4at  40070  lplncvrlvol  40073  2lplnj  40077  dalemcea  40117  dalem3  40121  psubspi  40204  linepsubN  40209  elpmap  40215  pmapsub  40225  lnatexN  40236  cdlema1N  40248  cdlemb  40251  elpadd  40256  paddvaln0N  40258  paddasslem5  40281  llnexchb2lem  40325  llnexch2N  40327  islhp  40453  lhpat3  40503  4atexlemex2  40528  4atex  40533  4atex2-0aOLDN  40535  4atex2-0cOLDN  40537  lautle  40541  lautcvr  40549  lauteq  40552  ldilval  40570  ltrnu  40578  trlval2  40620  trlne  40642  cdleme0ex1N  40680  cdleme0nex  40747  cdleme18d  40752  cdlemednuN  40757  cdleme25b  40811  cdleme25cv  40815  cdleme27b  40825  cdleme29b  40832  cdleme31sn  40837  cdleme31fv  40847  cdleme31fv2  40850  cdlemefrs29bpre0  40853  cdlemefr29bpre0N  40863  cdlemefr29clN  40864  cdlemefr32fvaN  40866  cdlemefr32fva1  40867  cdlemefs29pre00N  40869  cdlemefs32sn1aw  40871  cdlemefs29bpre0N  40873  cdlemefs29bpre1N  40874  cdlemefs29cpre1N  40875  cdlemefs29clN  40876  cdlemefs32fvaN  40879  cdlemefs32fva1  40880  cdleme41sn3a  40890  cdleme32fva  40894  cdleme32e  40902  cdleme35f  40911  cdleme40v  40926  cdleme42b  40935  trlord  41026  cdlemg1cex  41045  diaval  41489  diaeldm  41493  diaelrnN  41502  cdlemm10N  41575  dibglbN  41623  dicval  41633  dicfnN  41640  dicvalrelN  41642  dihval  41689  dihlsscpre  41691  dihglblem3N  41752  dihmeetlem2N  41756  djhcvat42  41872  lcmineqlem4  42482  aks4d1p4  42529  aks4d1p5  42530  aks4d1p7  42533  aks4d1p8d2  42535  aks4d1p8  42537  hashnexinjle  42579  sticksstones1  42596  sticksstones2  42597  sticksstones10  42605  sticksstones12a  42607  aks6d1c7lem4  42633  aks6d1c7  42634  grpods  42644  unitscyglem2  42646  unitscyglem3  42647  unitscyglem4  42648  qsalrel  42691  supinf  42692  dvdsexpnn0  42777  redvmptabs  42803  sn-nnne0  42916  sn-sup2  42947  fimgmcyclem  42989  flt4lem2  43091  flt4lem7  43103  lzenom  43213  fphpdo  43260  irrapxlem4  43268  pellexlem6  43277  infmrgelbi  43321  pellfundre  43324  pellfundlb  43327  monotoddzz  43386  zindbi  43389  jm2.27  43451  rmydioph  43457  rpnnen3lem  43474  fnwe2lem2  43494  aomclem8  43504  hbtlem5  43571  hbt  43573  sdomne0  43855  sdomne0d  43856  ensucne0  43971  sucomisnotcard  43986  en2pr  43989  pr2cv  43990  refimssco  44049  rfovfvfvd  44445  rfovcnvf1od  44446  fsovrfovd  44451  nzss  44759  relprel  45393  permaxinf2lem  45454  wessf1ornlem  45630  axccdom  45666  dmrelrnrel  45670  axccd  45673  rnmptlb  45687  rnmptbdd  45689  rnmptbd2  45693  rnmptbdlem  45699  rnmptbd  45700  dstregt0  45730  suplesup  45784  supxrunb3  45843  supxrleubrnmpt  45849  rexabslelem  45861  rexabsle  45862  suprleubrnmpt  45865  infrnmptle  45866  infxrunb3rnmpt  45871  infxrpnf  45889  supminfxr  45907  infrpgernmpt  45908  xrpnf  45928  limsupre  46084  limsupref  46128  limsupbnd1f  46129  limsuppnfd  46145  climinf2  46150  limsuppnf  46154  climinfmpt  46158  climinf3  46159  limsupmnflem  46163  limsupmnf  46164  limsupre2  46168  limsupmnfuzlem  46169  limsupre2mpt  46173  limsupre3lem  46175  limsupre3  46176  limsupre3mpt  46177  limsupre3uzlem  46178  limsupre3uz  46179  limsupreuz  46180  limsupreuzmpt  46182  liminfval2  46211  liminfreuzlem  46245  liminfreuz  46246  xlimpnfxnegmnf  46257  cnrefiisplem  46272  xlimpnfv  46281  xlimpnf  46285  xlimpnfmpt  46287  dfxlim2  46291  icccncfext  46330  cncficcgt0  46331  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem5  46448  stoweidlem20  46463  stoweidlem26  46469  stoweidlem28  46471  stoweidlem29  46472  stoweidlem34  46477  wallispilem3  46510  stirlinglem13  46529  fourierdlem41  46591  fourierdlem42  46592  fourierdlem51  46600  fourierdlem54  46603  salunicl  46759  saluncl  46760  salexct  46777  salexct2  46782  salexct3  46785  salgencntex  46786  salgensscntex  46787  sge0pnffigt  46839  meadjuni  46900  omeunile  46948  ovnlerp  47005  hoidifhspval  47051  ovolval5lem2  47096  salpreimagelt  47150  pimincfltioo  47161  salpreimagtge  47168  salpreimagtlt  47173  incsmf  47185  issmfgt  47199  smfpreimagt  47205  decsmf  47210  issmfge  47213  smfpimgtxr  47223  smfpreimage  47225  smfinflem  47260  smfinf  47261  finfdm  47289  funressnfv  47488  funressnvmo  47490  funressnmo  47491  dfdfat2  47573  tz6.12-afv  47618  funressndmafv2rn  47668  tz6.12-afv2  47685  dfatcolem  47700  dfatco  47701  zplusmodne  47794  m1modne  47799  minusmod5ne  47800  submodneaddmod  47802  modmknepk  47813  iccpartigtl  47880  iccpartgt  47884  icceuelpartlem  47892  iccpartnel  47895  sprsymrelfolem2  47950  nprmmul2  47985  goldbachthlem2  48006  odz2prm2pw  48023  fmtnoprmfac1  48025  fmtnoprmfac2  48027  fmtnofac2  48029  fmtno4prmfac  48032  fmtno4prm  48035  prmdvdsfmtnof1lem1  48044  31prm  48057  nprmdvdsfacm1  48084  perfectALTVlem2  48195  nnsum3primes4  48261  nnsum3primesprm  48263  nnsum3primesgbe  48265  nnsum3primesle9  48267  nnsum4primeseven  48273  nnsum4primesevenALTV  48274  wtgoldbnnsum4prm  48275  bgoldbnnsum3prm  48277  bgoldbtbndlem4  48281  bgoldbtbnd  48282  tgblthelfgott  48288  tgoldbach  48290  assintop  48682  isassintop  48683  assintopcllaw  48685  ztprmneprm  48820  ply1mulgsumlem1  48859  ply1mulgsumlem2  48860  lco0  48900  lcoel0  48901  lincsumcl  48904  lincscmcl  48905  lcoss  48909  linindslinci  48921  lindslinindsimp1  48930  linds0  48938  el0ldep  48939  lindsrng01  48941  ldepspr  48946  islindeps2  48956  isldepslvec2  48958  zlmodzxzldep  48977  ldepsnlinc  48981  elbigo2r  49026  xpco2  49329  tposres0  49349  lubsscl  49432  glbsscl  49433  lubprlem  49434  ipolub  49460  ipoglb  49463  catprslem  49482  infsubc2  49533  nelsubc3lem  49542  cnelsubclem  50075  setrec2lem1  50165