Theorem breq1 5077

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 4806	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2820	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 5075	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 5075	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075

This theorem is referenced by:  breq12  5079  breq1i  5081  breq1d  5084  nbrne2  5094  brab1  5122  pocl  5536  swopolem  5538  swopo  5539  po2ne  5544  solin  5555  sotrieq  5559  sotr2  5562  isso2i  5565  somo  5567  dffr2  5581  frc  5583  frirr  5596  fr2nr  5597  wereu2  5617  vtoclr  5683  frsn  5708  brcog  5810  brcogw  5812  brcnvg  5823  dfdmf  5840  eldmg  5842  dmun  5854  dm0rn0  5868  dfrnf  5894  dmcosseq  5922  dmcosseqOLD  5923  dfres2  5995  imasng  6038  cotrg  6063  cnvsym  6066  asymref2  6069  sotri2  6081  somin1  6085  rnco  6205  coi1  6216  predtrss  6275  frpomin  6293  dffun2  6497  dffun6f  6502  funmo  6503  fun11  6561  fveq2  6829  eliman0  6866  nfunsn  6868  dffv2  6924  fvopab5  6970  dff3  7041  f1ompt  7052  fmptco  7071  dff13  7198  foeqcnvco  7244  isorel  7270  soisores  7271  soisoi  7272  isocnv  7274  isotr  7280  isomin  7281  isoini  7282  isopolem  7289  isosolem  7291  f1oiso  7295  f1oiso2  7296  weniso  7298  eqfunresadj  7304  caovordig  7561  caovordg  7563  caovord3d  7566  caovord  7567  caovord3  7569  caofrss  7659  caoftrn  7661  fr3nr  7715  dfwe2  7717  f1oweALT  7914  frxp  8065  poxp  8067  fnse  8072  poxp2  8082  frxp2  8083  poxp3  8089  frxp3  8090  xpord3pred  8091  poseq  8097  brtpos2  8171  rntpos  8178  tpostpos  8185  frrlem12  8236  ertr  8648  ecopovsym  8755  ecopovtrn  8756  isfi  8911  en0  8954  en0ALT  8955  en1  8960  endisj  8991  xpcomco  8994  sbth  9024  2pwne  9060  disjenex  9062  ssenen  9078  findcard  9087  findcard2  9088  pssnn  9092  sbthfi  9122  nneneq  9129  php  9130  onomeneq  9137  sdom1  9149  1sdom2dom  9153  isinf  9164  fineqvlem  9165  en1eqsnbi  9175  findcard3  9182  frfi  9184  fiint  9226  mapfienlem1  9307  mapfienlem2  9308  mapfienlem3  9309  mapfien  9310  marypha1lem  9335  supmo  9354  eqsup  9358  supub  9361  suplub  9362  suppr  9374  supisolem  9376  supisoex  9377  infmin  9398  infmo  9399  fiinfg  9403  fiinf2g  9404  infpr  9407  ordtypecbv  9421  ordtypelem3  9424  ordtypelem6  9427  ordtypelem7  9428  ordtypelem9  9430  ordtypelem10  9431  hartogslem1  9446  hartogs  9448  wemaplem1  9450  wemaplem2  9451  wemapso2lem  9456  card2on  9458  card2inf  9459  elharval  9465  brwdom2  9477  wdomtr  9479  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  21436  prmirredlem  21441  znleval  21523  frlmelbas  21725  ellspd  21771  islindf4  21807  psrbagconcl  21896  psrbagleadd1  21897  gsumbagdiaglem  21899  rhmpsrlem2  21909  psrlidm  21929  psrridm  21930  psrass1  21931  psrcom  21935  mplelbas  21958  mplmonmul  22003  ltbwe  22011  mhpmulcl  22104  psdmul  22121  coe1fsupp  22166  coe1ae0  22168  coe1mul2  22222  coe1tmmul  22230  pmatcoe1fsupp  22654  chfacffsupp  22809  chfacfscmulfsupp  22812  chfacfscmulgsum  22813  chfacfpmmulfsupp  22816  chfacfpmmulgsum  22817  ordtbas2  23144  ordtopn2  23148  ordtrest2lem  23156  pnfnei  23173  ordtt1  23332  ordthauslem  23336  2ndci  23401  2ndcsb  23402  2ndcredom  23403  2ndc1stc  23404  1stcrest  23406  2ndcctbss  23408  2ndcdisj  23409  2ndcsep  23412  lly1stc  23449  tx1stc  23603  ordthmeolem  23754  ufildom1  23879  xmetrtri2  24309  prdsxmetlem  24321  ssblex  24381  prdsbl  24444  comet  24466  stdbdxmet  24468  stdbdmopn  24471  met1stc  24474  dscmet  24525  metdstri  24805  metdscn  24810  xrhmeo  24901  bndth  24913  evth  24914  lebnumlem3  24918  pcovalg  24967  pco1  24970  pcocn  24972  pcopt  24977  pcopt2  24978  pcoass  24979  nmoleub3  25074  bcthlem5  25283  rrxfsupp  25357  minveclem4c  25380  minveclem2  25381  minveclem3b  25383  minveclem4  25387  minveclem6  25389  pmltpclem1  25403  pmltpc  25405  ovollb2lem  25443  ovolctb  25445  ovolunlem1  25452  ovoliunlem1  25457  ovoliunlem2  25458  ovoliun2  25461  ovolshftlem1  25464  ovolscalem1  25468  ovolicc1  25471  ovolicc2lem3  25474  voliunlem2  25506  voliunlem3  25507  ioombl1lem4  25516  uniioovol  25534  uniioombllem2  25538  uniioombllem3  25540  uniioombllem6  25543  volsup2  25560  ismbfd  25594  mbfsup  25619  mbflimsup  25621  itg1climres  25669  mbfi1fseqlem4  25673  itg2lr  25685  itg2leub  25689  itg2seq  25697  itg2monolem1  25705  itg2monolem3  25707  itg2mono  25708  itg2i1fseq2  25711  itg2gt0  25715  itg2cnlem1  25716  itg2cnlem2  25717  itg2cn  25718  iblss  25760  itgless  25772  ibladdlem  25775  iblabsr  25785  iblmulc2  25786  itgabs  25790  bddiblnc  25797  ditgeq1  25803  dvferm2lem  25941  rolle  25945  dvlip2  25950  c1liplem1  25951  c1lip1  25952  dvfsumlem2  25982  dvfsumlem4  25984  mdegleb  26017  degltlem1  26025  plyco0  26145  plyeq0lem  26163  coeeq2  26195  dgrle  26196  dgradd2  26221  plydiveu  26252  aareccl  26280  aalioulem2  26287  aaliou3lem7  26303  psercnlem1  26378  pilem2  26405  pilem3  26406  logltb  26552  divlogrlim  26587  logcnlem3  26596  cxpaddlelem  26703  rlimcnp  26917  cxplim  26923  cxploglim  26929  scvxcvx  26937  ftalem1  27024  ftalem2  27025  isppw2  27066  vmappw  27067  sgmnncl  27098  sqff1o  27133  fsumdvdsdiaglem  27134  dvdsppwf1o  27137  dvdsflsumcom  27139  musum  27142  muinv  27144  mpodvdsmulf1o  27145  dvdsmulf1o  27147  vmalelog  27156  vmasum  27167  logfac2  27168  perfectlem2  27181  bcmono  27228  bpos1lem  27233  bposlem9  27243  lgsmod  27274  lgsne0  27286  gausslemma2dlem4  27320  2sqlem6  27374  2sqlem8  27377  2sqlem10  27379  2sqreulem1  27397  2sqreunnlem1  27400  chtppilim  27426  rpvmasumlem  27438  dchrisumlema  27439  dchrisumlem2  27441  dchrvmasumlem1  27446  dchrvmasumiflem1  27452  dchrisum0flblem1  27459  dchrisum0flblem2  27460  dchrisum0  27471  rplogsum  27478  logsqvma  27493  pntpbnd1  27537  pntpbnd2  27538  pntibndlem3  27543  pntlemj  27554  pntlemi  27555  pntlem3  27560  pnt3  27563  ostth3  27589  nodense  27644  noresle  27649  nosupprefixmo  27652  noinfprefixmo  27653  nosupcbv  27654  nosupdm  27656  nosupbnd1lem1  27660  nosupbnd1lem4  27663  nosupbnd1  27666  nosupbnd2lem1  27667  nosupbnd2  27668  noinfcbv  27669  noinfdm  27671  noinffv  27673  noinfres  27674  noinfbnd1lem3  27677  noinfbnd1lem4  27678  noinfbnd1lem5  27679  noinfbnd1  27681  noetalem2  27694  nocvxminlem  27734  sltssnb  27749  sltssepc  27751  conway  27759  cutsval  27760  etaslts  27773  lesrec  27779  eqcuts3  27784  bday1  27794  cuteq1  27797  madeval2  27813  rightval  27830  elleft  27831  sltsright  27841  made0  27843  madecut  27863  left1s  27875  madebdaylemlrcut  27879  ltslpss  27888  cofslts  27898  coinitslts  27899  cofcutr  27904  cofcutrtime  27907  cofss  27910  coiniss  27911  cutmax  27914  cutmin  27915  cutminmax  27916  addsproplem1  27949  addsprop  27956  leadds1  27969  addsuniflem  27981  negsproplem1  28008  negsprop  28015  negsid  28021  negsunif  28035  mulsproplemcbv  28095  mulsproplem1  28096  mulsproplem9  28104  mulsprop  28110  sltmuls1  28127  sltmuls2  28128  mulsuniflem  28129  precsexlem11  28197  abslts  28229  oncutlt  28244  oniso  28251  bdayons  28256  addonbday  28259  n0fincut  28335  onsfi  28336  n0subs  28343  bdayn0p1  28349  eucliddivs  28356  zcuts  28387  twocut  28403  halfcut  28438  addhalfcut  28439  bdaypw2n0bndlem  28443  bdayfinbndcbv  28446  bdayfinbndlem1  28447  bdayfinbndlem2  28448  z12bdaylem1  28450  elreno  28471  elreno2  28475  tgjustc1  28531  tgjustc2  28532  iscgrglt  28570  tgcgr4  28587  hlcgreu  28674  lmif  28841  islmib  28843  trgcopyeu  28862  iscgrad  28867  inaghl  28901  axlowdim2  29017  axlowdim  29018  axcontlem2  29022  axcontlem3  29023  axcontlem4  29024  axcontlem7  29027  axcontlem9  29029  axcontlem10  29030  axcontlem11  29031  axcontlem12  29032  ebtwntg  29039  umgrupgr  29160  nbusgrvtxm1  29436  crctcshwlkn0lem2  29867  crctcshwlkn0lem3  29868  crctcsh  29880  wlkswwlksf1o  29935  clwlkclwwlklem2fv1  30053  clwlkclwwlkf  30066  0clwlkv  30189  eupth2  30297  numclwwlk5  30446  nmoubi  30831  minvecolem2  30934  minvecolem3  30935  minvecolem4c  30938  minvecolem4  30939  minvecolem5  30940  minvecolem6  30941  htthlem  30976  chlimi  31293  chcompl  31301  hsn0elch  31307  cmbr3  31667  cmcm  31673  cmcm3  31674  lecm  31676  nmopub  31967  nmfnleub  31984  nmopun  32073  nmcexi  32085  cnlnadjlem7  32132  pjnmopi  32207  stle0i  32298  stlesi  32300  stm1i  32302  csmdsymi  32393  cvmd  32395  atcveq0  32407  atcv1  32439  atord  32447  atcvat2  32448  chirred  32454  mdsym  32471  mddmdin0i  32490  cdj1i  32492  fmptcof2  32718  fnpreimac  32731  isoun  32763  fcobijfs  32782  fcobijfs2  32783  lt2addrd  32811  xlt2addrd  32820  xrge0infss  32821  infxrge0glb  32826  xrofsup  32828  fz1nnct  32862  sgnmulsgn  32903  toslublem  33020  tosglblem  33022  ismntd  33032  mgccole1  33038  mgccole2  33039  mgcmnt1  33040  mgcmnt2  33041  dfmgc2lem  33043  dfmgc2  33044  psgnfzto1stlem  33149  fzto1st  33152  psgnfzto1st  33154  trsp2cyc  33172  xrnarchi  33233  archirng  33237  archiexdiv  33239  archiabl  33247  isarchiofld  33248  elrgspnlem1  33291  elrgspnlem2  33292  elrgspnlem3  33293  elrgspnlem4  33294  elrgspn  33295  elrgspnsubrunlem1  33296  elrgspnsubrunlem2  33297  elrgspnsubrun  33298  linds2eq  33429  elrspunidl  33476  elrspunsn  33477  isrprm  33565  evl1deg1  33624  evl1deg2  33625  evl1deg3  33626  extvfvvcl  33667  extvfvcl  33668  mplmulmvr  33671  evlextv  33674  mplvrpmlem  33675  mplvrpmfgalem  33676  mplvrpmga  33677  mplvrpmmhm  33678  mplvrpmrhm  33679  psrmonmul  33682  psrmonprod  33684  esplyfval0  33696  esplylem  33698  esplyfv1  33701  esplyfval3  33704  esplyfvaln  33706  esplyind  33707  ply1degltdimlem  33754  lbsdiflsp0  33758  fedgmullem1  33761  fedgmullem2  33762  fedgmul  33763  fldextrspunlsplem  33805  fldextrspunlsp  33806  smatrcl  33928  smatlem  33929  madjusmdetlem2  33960  madjusmdet  33963  cmpcref  33982  ldlfcntref  33986  dispcmp  33991  zarcmplem  34013  ordtrest2NEWlem  34054  ordtconnlem1  34056  xrge0iifiso  34067  rge0scvg  34081  gsumesum  34191  esumfsup  34202  esumpinfval  34205  esumpcvgval  34210  esumcvg  34218  sigaclcu  34249  sigaclci  34264  unelsiga  34266  unelldsys  34290  sigapildsys  34294  ldgenpisyslem1  34295  fiunelros  34306  measvun  34341  voliune  34361  volfiniune  34362  oms0  34429  omssubaddlem  34431  omssubadd  34432  carsgsigalem  34447  carsgclctunlem2  34451  carsgclctun  34453  pmeasmono  34456  pmeasadd  34457  orvcval2  34591  dstfrvel  34606  ballotlemfc0  34625  ballotlemfcc  34626  ballotlemsv  34642  ballotlemsf1o  34646  breprexp  34765  tgoldbachgt  34795  bnj23  34849  bnj1185  34923  bnj1152  35128  bnj1418  35170  fnrelpredd  35222  loop1cycl  35307  umgr2cycl  35311  acycgrcycl  35317  dfdm5  35943  dfrn5  35944  wzel  35992  wsuclem  35993  brpprod  36053  brsset  36057  brbigcup  36066  dffix2  36073  elfuns  36083  brimageg  36095  brdomaing  36103  brrangeg  36104  brimg  36105  brapply  36106  lemsuccf  36109  funpartlem  36112  brrestrict  36119  dfrecs2  36120  dfrdg4  36121  brofs  36175  btwncomim  36183  btwnintr  36189  btwnexch3  36190  btwnexch2  36193  brifs  36213  brcolinear2  36228  colineardim1  36231  brfs  36249  btwnconn1  36271  segcon2  36275  seglerflx  36282  seglemin  36283  btwnsegle  36287  colinbtwnle  36288  broutsideof2  36292  fvray  36311  lineunray  36317  lineelsb2  36318  linerflx1  36319  trer  36486  elicc3  36487  finminlem  36488  nn0prpwlem  36492  nn0prpw  36493  fnessref  36527  refssfne  36528  weiunlem  36633  weiunfrlem  36634  weiunfr  36637  weiunse  36638  unblimceq0lem  36754  unblimceq0  36755  unbdqndv2  36759  knoppndvlem21  36780  taupilemrplb  37622  dfgcd3  37626  icorempo  37655  icoreval  37657  iooelexlt  37666  relowlssretop  37667  domalom  37708  ctbssinf  37710  pibt2  37721  phpreu  37913  fin2solem  37915  fin2so  37916  ltflcei  37917  ptrecube  37929  poimirlem1  37930  poimirlem2  37931  poimirlem5  37934  poimirlem6  37935  poimirlem7  37936  poimirlem9  37938  poimirlem12  37941  poimirlem22  37951  poimirlem23  37952  poimirlem24  37953  poimirlem26  37955  poimirlem27  37956  poimirlem32  37961  heicant  37964  mblfinlem1  37966  mblfinlem2  37967  itg2addnclem  37980  itg2addnclem3  37982  itg2addnc  37983  itg2gt0cn  37984  ibladdnclem  37985  iblmulc2nc  37994  itgabsnc  37998  ftc1anclem5  38006  ftc1anclem7  38008  ftc1anclem8  38009  ftc1anc  38010  indexdom  38043  filbcmb  38049  fdc  38054  prdsbnd  38102  heiborlem3  38122  rrnequiv  38144  rngoueqz  38249  eqbrtr  38547  elrnressn  38589  inxprnres  38607  presucmap  38804  eqvreltr  39000  prtlem10  39299  lsatcveq0  39466  lsatcv1  39482  oposlem  39616  opnlen0  39622  lub0N  39623  glb0N  39627  omllaw  39677  cmtbr4N  39689  cvrval  39703  cvrnbtwn  39705  cvrnbtwn2  39709  cvrnbtwn3  39710  cvrcon3b  39711  cvrnbtwn4  39713  atcvreq0  39748  atnle  39751  atlatmstc  39753  cvlexch1  39762  glbconN  39811  hlsuprexch  39815  exatleN  39838  cvratlem  39855  atcvrj0  39862  atcvrj2b  39866  atlelt  39872  cvrat4  39877  3dim1lem5  39900  3dim2  39902  3dim3  39903  ps-2  39912  llni  39942  llnn0  39950  llnle  39952  lplni  39966  lplni2  39971  lplnle  39974  lplnn0N  39981  llncvrlpln  39992  2llnjN  40001  lvoli  40009  lvoli3  40011  lvoli2  40015  lvoln0N  40025  4at  40047  lplncvrlvol  40050  2lplnj  40054  dalemcea  40094  dalem3  40098  psubspi  40181  linepsubN  40186  elpmap  40192  pmapsub  40202  lnatexN  40213  cdlema1N  40225  cdlemb  40228  elpadd  40233  paddvaln0N  40235  paddasslem5  40258  llnexchb2lem  40302  llnexch2N  40304  islhp  40430  lhpat3  40480  4atexlemex2  40505  4atex  40510  4atex2-0aOLDN  40512  4atex2-0cOLDN  40514  lautle  40518  lautcvr  40526  lauteq  40529  ldilval  40547  ltrnu  40555  trlval2  40597  trlne  40619  cdleme0ex1N  40657  cdleme0nex  40724  cdleme18d  40729  cdlemednuN  40734  cdleme25b  40788  cdleme25cv  40792  cdleme27b  40802  cdleme29b  40809  cdleme31sn  40814  cdleme31fv  40824  cdleme31fv2  40827  cdlemefrs29bpre0  40830  cdlemefr29bpre0N  40840  cdlemefr29clN  40841  cdlemefr32fvaN  40843  cdlemefr32fva1  40844  cdlemefs29pre00N  40846  cdlemefs32sn1aw  40848  cdlemefs29bpre0N  40850  cdlemefs29bpre1N  40851  cdlemefs29cpre1N  40852  cdlemefs29clN  40853  cdlemefs32fvaN  40856  cdlemefs32fva1  40857  cdleme41sn3a  40867  cdleme32fva  40871  cdleme32e  40879  cdleme35f  40888  cdleme40v  40903  cdleme42b  40912  trlord  41003  cdlemg1cex  41022  diaval  41466  diaeldm  41470  diaelrnN  41479  cdlemm10N  41552  dibglbN  41600  dicval  41610  dicfnN  41617  dicvalrelN  41619  dihval  41666  dihlsscpre  41668  dihglblem3N  41729  dihmeetlem2N  41733  djhcvat42  41849  lcmineqlem4  42459  aks4d1p4  42506  aks4d1p5  42507  aks4d1p7  42510  aks4d1p8d2  42512  aks4d1p8  42514  hashnexinjle  42556  sticksstones1  42573  sticksstones2  42574  sticksstones10  42582  sticksstones12a  42584  aks6d1c7lem4  42610  aks6d1c7  42611  grpods  42621  unitscyglem2  42623  unitscyglem3  42624  unitscyglem4  42625  qsalrel  42668  supinf  42669  dvdsexpnn0  42754  redvmptabs  42780  sn-nnne0  42893  sn-sup2  42924  fimgmcyclem  42966  flt4lem2  43068  flt4lem7  43080  lzenom  43190  fphpdo  43233  irrapxlem4  43241  pellexlem6  43250  infmrgelbi  43294  pellfundre  43297  pellfundlb  43300  monotoddzz  43359  zindbi  43362  jm2.27  43424  rmydioph  43430  rpnnen3lem  43447  fnwe2lem2  43467  aomclem8  43477  hbtlem5  43544  hbt  43546  sdomne0  43828  sdomne0d  43829  ensucne0  43944  sucomisnotcard  43959  en2pr  43962  pr2cv  43963  refimssco  44022  rfovfvfvd  44418  rfovcnvf1od  44419  fsovrfovd  44424  nzss  44732  relprel  45366  permaxinf2lem  45427  wessf1ornlem  45603  axccdom  45639  dmrelrnrel  45643  axccd  45646  rnmptlb  45660  rnmptbdd  45662  rnmptbd2  45666  rnmptbdlem  45672  rnmptbd  45673  dstregt0  45703  suplesup  45757  supxrunb3  45816  supxrleubrnmpt  45822  rexabslelem  45834  rexabsle  45835  suprleubrnmpt  45838  infrnmptle  45839  infxrunb3rnmpt  45844  infxrpnf  45862  supminfxr  45880  infrpgernmpt  45881  xrpnf  45901  limsupre  46057  limsupref  46101  limsupbnd1f  46102  limsuppnfd  46118  climinf2  46123  limsuppnf  46127  climinfmpt  46131  climinf3  46132  limsupmnflem  46136  limsupmnf  46137  limsupre2  46141  limsupmnfuzlem  46142  limsupre2mpt  46146  limsupre3lem  46148  limsupre3  46149  limsupre3mpt  46150  limsupre3uzlem  46151  limsupre3uz  46152  limsupreuz  46153  limsupreuzmpt  46155  liminfval2  46184  liminfreuzlem  46218  liminfreuz  46219  xlimpnfxnegmnf  46230  cnrefiisplem  46245  xlimpnfv  46254  xlimpnf  46258  xlimpnfmpt  46260  dfxlim2  46264  icccncfext  46303  cncficcgt0  46304  ioodvbdlimc1lem2  46348  ioodvbdlimc2lem  46350  stoweidlem5  46421  stoweidlem20  46436  stoweidlem26  46442  stoweidlem28  46444  stoweidlem29  46445  stoweidlem34  46450  wallispilem3  46483  stirlinglem13  46502  fourierdlem41  46564  fourierdlem42  46565  fourierdlem51  46573  fourierdlem54  46576  salunicl  46732  saluncl  46733  salexct  46750  salexct2  46755  salexct3  46758  salgencntex  46759  salgensscntex  46760  sge0pnffigt  46812  meadjuni  46873  omeunile  46921  ovnlerp  46978  hoidifhspval  47024  ovolval5lem2  47069  salpreimagelt  47123  pimincfltioo  47134  salpreimagtge  47141  salpreimagtlt  47146  incsmf  47158  issmfgt  47172  smfpreimagt  47178  decsmf  47183  issmfge  47186  smfpimgtxr  47196  smfpreimage  47198  smfinflem  47233  smfinf  47234  finfdm  47262  funressnfv  47479  funressnvmo  47481  funressnmo  47482  dfdfat2  47564  tz6.12-afv  47609  funressndmafv2rn  47659  tz6.12-afv2  47676  dfatcolem  47691  dfatco  47692  zplusmodne  47785  m1modne  47790  minusmod5ne  47791  submodneaddmod  47793  modmknepk  47804  iccpartigtl  47871  iccpartgt  47875  icceuelpartlem  47883  iccpartnel  47886  sprsymrelfolem2  47941  nprmmul2  47976  goldbachthlem2  47997  odz2prm2pw  48014  fmtnoprmfac1  48016  fmtnoprmfac2  48018  fmtnofac2  48020  fmtno4prmfac  48023  fmtno4prm  48026  prmdvdsfmtnof1lem1  48035  31prm  48048  nprmdvdsfacm1  48075  perfectALTVlem2  48186  nnsum3primes4  48252  nnsum3primesprm  48254  nnsum3primesgbe  48256  nnsum3primesle9  48258  nnsum4primeseven  48264  nnsum4primesevenALTV  48265  wtgoldbnnsum4prm  48266  bgoldbnnsum3prm  48268  bgoldbtbndlem4  48272  bgoldbtbnd  48273  tgblthelfgott  48279  tgoldbach  48281  assintop  48673  isassintop  48674  assintopcllaw  48676  ztprmneprm  48811  ply1mulgsumlem1  48850  ply1mulgsumlem2  48851  lco0  48891  lcoel0  48892  lincsumcl  48895  lincscmcl  48896  lcoss  48900  linindslinci  48912  lindslinindsimp1  48921  linds0  48929  el0ldep  48930  lindsrng01  48932  ldepspr  48937  islindeps2  48947  isldepslvec2  48949  zlmodzxzldep  48968  ldepsnlinc  48972  elbigo2r  49017  xpco2  49320  tposres0  49340  lubsscl  49423  glbsscl  49424  lubprlem  49425  ipolub  49451  ipoglb  49454  catprslem  49473  infsubc2  49524  nelsubc3lem  49533  cnelsubclem  50066  setrec2lem1  50156