Theorem breq1 5102

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  breq12  5104  breq1i  5106  breq1d  5109  nbrne2  5119  brab1  5147  pocl  5541  swopolem  5543  swopo  5544  po2ne  5549  solin  5560  sotrieq  5564  sotr2  5567  isso2i  5570  somo  5572  dffr2  5586  frc  5588  frirr  5601  fr2nr  5602  wereu2  5622  vtoclr  5688  frsn  5713  brcog  5816  brcogw  5818  brcnvg  5829  dfdmf  5846  eldmg  5848  dmun  5860  dm0rn0  5874  dfrnf  5900  dmcosseq  5928  dmcosseqOLD  5929  dfres2  6001  imasng  6044  cotrg  6069  cnvsym  6072  asymref2  6075  sotri2  6087  somin1  6091  rnco  6211  coi1  6222  predtrss  6281  frpomin  6299  dffun2  6503  dffun6f  6508  funmo  6509  fun11  6567  fveq2  6835  eliman0  6872  nfunsn  6874  dffv2  6930  fvopab5  6976  dff3  7047  f1ompt  7058  fmptco  7076  dff13  7202  foeqcnvco  7248  isorel  7274  soisores  7275  soisoi  7276  isocnv  7278  isotr  7284  isomin  7285  isoini  7286  isopolem  7293  isosolem  7295  f1oiso  7299  f1oiso2  7300  weniso  7302  eqfunresadj  7308  caovordig  7565  caovordg  7567  caovord3d  7570  caovord  7571  caovord3  7573  caofrss  7663  caoftrn  7665  fr3nr  7719  dfwe2  7721  f1oweALT  7918  frxp  8070  poxp  8072  fnse  8077  poxp2  8087  frxp2  8088  poxp3  8094  frxp3  8095  xpord3pred  8096  poseq  8102  brtpos2  8176  rntpos  8183  tpostpos  8190  frrlem12  8241  ertr  8653  ecopovsym  8760  ecopovtrn  8761  isfi  8916  en0  8959  en0ALT  8960  en1  8965  endisj  8996  xpcomco  8999  sbth  9029  2pwne  9065  disjenex  9067  ssenen  9083  findcard  9092  findcard2  9093  pssnn  9097  sbthfi  9127  nneneq  9134  php  9135  onomeneq  9142  sdom1  9154  1sdom2dom  9158  isinf  9169  fineqvlem  9170  en1eqsnbi  9180  findcard3  9187  frfi  9189  fiint  9231  mapfienlem1  9312  mapfienlem2  9313  mapfienlem3  9314  mapfien  9315  marypha1lem  9340  supmo  9359  eqsup  9363  supub  9366  suplub  9367  suppr  9379  supisolem  9381  supisoex  9382  infmin  9403  infmo  9404  fiinfg  9408  fiinf2g  9409  infpr  9412  ordtypecbv  9426  ordtypelem3  9429  ordtypelem6  9432  ordtypelem7  9433  ordtypelem9  9435  ordtypelem10  9436  hartogslem1  9451  hartogs  9453  wemaplem1  9455  wemaplem2  9456  wemapso2lem  9461  card2on  9463  card2inf  9464  elharval  9470  brwdom2  9482  wdomtr  9484  cantnfs  9579  cantnfp1lem2  9592  oemapso  9595  cantnflem1  9602  wemapwe  9610  ttrclss  9633  r111  9691  kardex  9810  karden  9811  isnumi  9862  tskwe  9866  cardid2  9869  cardonle  9873  cardne  9881  iscard2  9892  infxpenlem  9927  fodomfi2  9974  wdomfil  9975  wdomnumr  9978  alephsuc2  9994  infenaleph  10005  iunfictbso  10028  infpss  10130  cff1  10172  cfslb2n  10182  sornom  10191  fin4i  10212  isfin6  10214  isfin7  10215  isfin1-3  10300  fin1a2lem9  10322  fin1a2lem11  10324  hsmexlem4  10343  axcc2lem  10350  axcc4dom  10355  domtriomlem  10356  numthcor  10408  zorn2lem2  10411  zorn2lem3  10412  zorn2lem7  10416  zorn2g  10417  axdclem  10433  axdc  10435  brdom7disj  10445  brdom6disj  10446  uniimadom  10458  ondomon  10477  alephval2  10487  alephreg  10497  pwcfsdom  10498  elgch  10537  gchi  10539  fpwwe2lem11  10556  fpwwe2lem12  10557  winainflem  10608  winalim2  10611  tsken  10669  0tsk  10670  inar1  10690  tskord  10695  tskuni  10698  grudomon  10732  pinq  10842  nqereu  10844  enqeq  10849  ltbtwnnq  10893  ltrnq  10894  prcdnq  10908  prnmax  10910  genpnmax  10922  nqpr  10929  1idpr  10944  reclem2pr  10963  reclem3pr  10964  reclem4pr  10965  recexpr  10966  supexpr  10969  ltsosr  11009  1ne0sr  11011  ltasr  11015  supsrlem  11026  axpre-lttri  11080  axpre-lttrn  11081  axpre-ltadd  11082  axpre-sup  11084  lelttr  11227  dedekind  11300  dedekindle  11301  ltordlem  11666  lt0ne0d  11706  fimaxre3  12092  fiminre2  12094  lbreu  12096  lble  12098  sup2  12102  infm3  12105  suprleub  12112  supaddc  12113  supadd  12114  supmul1  12115  supmullem1  12116  supmul  12118  nnne0  12183  nnsub  12193  nominpos  12382  nnunb  12401  arch  12402  nn0sub  12455  nn0n0n1ge2b  12474  nn0lt10b  12558  zextle  12569  peano5uzti  12586  fzind  12594  btwnz  12599  uzval  12757  uzwo  12828  nnwof  12831  ublbneg  12850  lbzbi  12853  zsupss  12854  uzsupss  12857  uzwo3  12860  zmax  12862  rebtwnz  12864  rpnnen1lem3  12896  xrltnsym  13055  xrlttri  13057  xrlttr  13058  xrlelttr  13074  nltpnft  13083  xrmaxlt  13100  xrmaxle  13102  qbtwnre  13118  qbtwnxr  13119  xltnegi  13135  xnn0lenn0nn0  13164  xsubge0  13180  xlesubadd  13182  xmullem2  13184  xlemul1a  13207  xrinfmexpnf  13225  xrsupsslem  13226  xrinfmsslem  13227  xrub  13231  supxrunb1  13238  supxrunb2  13239  reltre  13260  rpltrp  13261  reltxrnmnf  13262  ixxval  13273  elixx1  13274  elioo2  13306  iccid  13310  icc0  13313  fzval  13429  elfz1  13432  elfznelfzo  13693  elfznelfzob  13694  flval  13718  fllelt  13721  flflp1  13731  flval2  13738  flval3  13739  flbi  13740  dfceil2  13763  ceilval2  13764  fleqceilz  13778  modid2  13822  addmodlteq  13873  fsequb2  13903  ssnn0fi  13912  seqf1olem2  13969  sqlecan  14136  faclbnd4lem1  14220  hashsnle1  14344  pr2pwpr  14406  hash3tpde  14420  rtrclreclem3  14987  relexpindlem  14990  sgnval  15015  01sqrexlem6  15174  01sqrex  15176  abslt  15242  absle  15243  rexanre  15274  rexico  15281  limsupgle  15404  limsupgre  15408  limsupbnd2  15410  rlim2lt  15424  rlim3  15425  ello12r  15444  ello1d  15450  elo12r  15455  rlimconst  15471  climshft  15503  rlimcn3  15517  o1rlimmul  15546  lo1le  15579  climsup  15597  caucvgrlem  15600  isumless  15772  divrcnv  15779  cvgrat  15810  rpnnen2lem10  16152  ruclem1  16160  ruclem2  16161  ruclem11  16169  ruclem12  16170  sqrt2irr  16178  absdvdsb  16205  dvdsle  16241  dvdsabseq  16244  dvdsdivcl  16247  dvdsext  16252  divalglem8  16331  divalglem9  16332  divalglem10  16333  divalgmod  16337  ndvdssub  16340  sadcaddlem  16388  gcdcllem1  16430  gcdcllem2  16431  gcdcllem3  16432  dfgcd2  16477  gcdzeq  16483  dvdssq  16498  nn0seqcvgd  16501  algcvgblem  16508  lcmval  16523  lcmdvds  16539  lcmgcdeq  16543  lcmfpr  16558  lcmf  16564  lcmftp  16567  lcmfunsnlem1  16568  lcmfunsnlem2lem1  16569  lcmfunsnlem2lem2  16570  lcmfdvdsb  16574  coprmgcdb  16580  coprmdvds1  16583  1nprm  16610  1idssfct  16611  isprm2lem  16612  isprm2  16613  dvdsprime  16618  nprm  16619  3prm  16625  dvdsprm  16634  exprmfct  16635  isprm5  16638  maxprmfct  16640  coprm  16642  prmdvdsncoprmbd  16658  ncoprmlnprm  16659  eulerthlem2  16713  phisum  16722  odzval  16723  pythagtriplem4  16751  pc2dvds  16811  pcprmpw2  16814  pcprmpw  16815  dvdsprmpweqle  16818  oddprmdvds  16835  prmpwdvds  16836  pockthg  16838  unbenlem  16840  prmreclem4  16851  prmreclem5  16852  prmreclem6  16853  1arith  16859  vdwlem6  16918  vdwlem11  16923  vdwlem13  16925  ramtlecl  16932  ramub  16945  rami  16947  ramubcl  16950  0ram  16952  ram0  16954  prmdvdsprmop  16975  prmolefac  16978  prmodvdslcmf  16979  prmgaplem2  16982  prmgaplcmlem1  16983  prmgaplcmlem2  16984  prmgaplem3  16985  prmgaplem4  16986  prmgaplem5  16987  prmgaplem6  16988  prmgapprmolem  16993  prmlem0  17037  prmlem1a  17038  imasaddfnlem  17453  imasvscafn  17462  imasleval  17466  prslem  18224  drsdir  18229  drsdirfi  18232  isdrs2  18233  posi  18244  posasymb  18246  pospropd  18252  pltval3  18264  plelttr  18269  pospo  18270  lubprop  18283  luble  18284  lublecllem  18285  glbprop  18296  joinval2lem  18305  joinlem  18308  meetlem  18322  meetle  18325  poslubmo  18336  posglbmo  18337  poslubd  18338  tleile  18346  latnlej  18383  isglbd  18436  lubub  18438  lubun  18442  clatleglb  18445  tsrlin  18512  letsr  18520  dirge  18530  pmtrval  19384  pmtrrn  19390  pmtrfrn  19391  pmtrrn2  19393  pmtrsn  19452  mndodcongi  19476  odeq  19483  odmulgeq  19490  gexnnod  19521  sylow1lem1  19531  pgpssslw  19547  sylow2a  19552  efgredeu  19685  efgred2  19686  gexex  19786  frgpnabllem2  19807  cyggenod  19817  dprdval  19938  dprdw  19945  dprdwd  19946  ablfacrplem  20000  ablfac1c  20006  ablfac1eu  20008  ablfaclem3  20022  omndadd  20061  abvtrivd  20769  zringlpir  21426  prmirredlem  21431  znleval  21513  frlmelbas  21715  ellspd  21761  islindf4  21797  psrbagconcl  21887  psrbagleadd1  21888  gsumbagdiaglem  21890  rhmpsrlem2  21901  psrlidm  21921  psrridm  21922  psrass1  21923  psrcom  21927  mplelbas  21950  mplmonmul  21995  ltbwe  22003  mhpmulcl  22096  psdmul  22113  coe1fsupp  22159  coe1ae0  22161  coe1mul2  22215  coe1tmmul  22223  pmatcoe1fsupp  22649  chfacffsupp  22804  chfacfscmulfsupp  22807  chfacfscmulgsum  22808  chfacfpmmulfsupp  22811  chfacfpmmulgsum  22812  ordtbas2  23139  ordtopn2  23143  ordtrest2lem  23151  pnfnei  23168  ordtt1  23327  ordthauslem  23331  2ndci  23396  2ndcsb  23397  2ndcredom  23398  2ndc1stc  23399  1stcrest  23401  2ndcctbss  23403  2ndcdisj  23404  2ndcsep  23407  lly1stc  23444  tx1stc  23598  ordthmeolem  23749  ufildom1  23874  xmetrtri2  24304  prdsxmetlem  24316  ssblex  24376  prdsbl  24439  comet  24461  stdbdxmet  24463  stdbdmopn  24466  met1stc  24469  dscmet  24520  metdstri  24800  metdscn  24805  xrhmeo  24904  bndth  24917  evth  24918  lebnumlem3  24922  pcovalg  24972  pco1  24975  pcocn  24977  pcopt  24982  pcopt2  24983  pcoass  24984  nmoleub3  25079  bcthlem5  25288  rrxfsupp  25362  minveclem4c  25385  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem6  25394  pmltpclem1  25409  pmltpc  25411  ovollb2lem  25449  ovolctb  25451  ovolunlem1  25458  ovoliunlem1  25463  ovoliunlem2  25464  ovoliun2  25467  ovolshftlem1  25470  ovolscalem1  25474  ovolicc1  25477  ovolicc2lem3  25480  voliunlem2  25512  voliunlem3  25513  ioombl1lem4  25522  uniioovol  25540  uniioombllem2  25544  uniioombllem3  25546  uniioombllem6  25549  volsup2  25566  ismbfd  25600  mbfsup  25625  mbflimsup  25627  itg1climres  25675  mbfi1fseqlem4  25679  itg2lr  25691  itg2leub  25695  itg2seq  25703  itg2monolem1  25711  itg2monolem3  25713  itg2mono  25714  itg2i1fseq2  25717  itg2gt0  25721  itg2cnlem1  25722  itg2cnlem2  25723  itg2cn  25724  iblss  25766  itgless  25778  ibladdlem  25781  iblabsr  25791  iblmulc2  25792  itgabs  25796  bddiblnc  25803  ditgeq1  25809  dvferm2lem  25950  rolle  25954  dvlip2  25960  c1liplem1  25961  c1lip1  25962  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem4  25996  mdegleb  26029  degltlem1  26037  plyco0  26157  plyeq0lem  26175  coeeq2  26207  dgrle  26208  dgradd2  26234  plydiveu  26266  aareccl  26294  aalioulem2  26301  aaliou3lem7  26317  psercnlem1  26395  pilem2  26422  pilem3  26423  logltb  26569  divlogrlim  26604  logcnlem3  26613  cxpaddlelem  26721  rlimcnp  26935  cxplim  26942  cxploglim  26948  scvxcvx  26956  ftalem1  27043  ftalem2  27044  isppw2  27085  vmappw  27086  sgmnncl  27117  sqff1o  27152  fsumdvdsdiaglem  27153  dvdsppwf1o  27156  dvdsflsumcom  27158  musum  27161  muinv  27163  mpodvdsmulf1o  27164  dvdsmulf1o  27166  vmalelog  27176  vmasum  27187  logfac2  27188  perfectlem2  27201  bcmono  27248  bpos1lem  27253  bposlem9  27263  lgsmod  27294  lgsne0  27306  gausslemma2dlem4  27340  2sqlem6  27394  2sqlem8  27397  2sqlem10  27399  2sqreulem1  27417  2sqreunnlem1  27420  chtppilim  27446  rpvmasumlem  27458  dchrisumlema  27459  dchrisumlem2  27461  dchrvmasumlem1  27466  dchrvmasumiflem1  27472  dchrisum0flblem1  27479  dchrisum0flblem2  27480  dchrisum0  27491  rplogsum  27498  logsqvma  27513  pntpbnd1  27557  pntpbnd2  27558  pntibndlem3  27563  pntlemj  27574  pntlemi  27575  pntlem3  27580  pnt3  27583  ostth3  27609  nodense  27664  noresle  27669  nosupprefixmo  27672  noinfprefixmo  27673  nosupcbv  27674  nosupdm  27676  nosupbnd1lem1  27680  nosupbnd1lem4  27683  nosupbnd1  27686  nosupbnd2lem1  27687  nosupbnd2  27688  noinfcbv  27689  noinfdm  27691  noinffv  27693  noinfres  27694  noinfbnd1lem3  27697  noinfbnd1lem4  27698  noinfbnd1lem5  27699  noinfbnd1  27701  noetalem2  27714  nocvxminlem  27754  sltssnb  27769  sltssepc  27771  conway  27779  cutsval  27780  etaslts  27793  lesrec  27799  eqcuts3  27804  bday1  27814  cuteq1  27817  madeval2  27833  rightval  27850  elleft  27851  sltsright  27861  made0  27863  madecut  27883  left1s  27895  madebdaylemlrcut  27899  ltslpss  27908  cofslts  27918  coinitslts  27919  cofcutr  27924  cofcutrtime  27927  cofss  27930  coiniss  27931  cutmax  27934  cutmin  27935  cutminmax  27936  addsproplem1  27969  addsprop  27976  leadds1  27989  addsuniflem  28001  negsproplem1  28028  negsprop  28035  negsid  28041  negsunif  28055  mulsproplemcbv  28115  mulsproplem1  28116  mulsproplem9  28124  mulsprop  28130  sltmuls1  28147  sltmuls2  28148  mulsuniflem  28149  precsexlem11  28217  abslts  28249  oncutlt  28264  oniso  28271  bdayons  28276  addonbday  28279  n0fincut  28355  onsfi  28356  n0subs  28363  bdayn0p1  28369  eucliddivs  28376  zcuts  28407  twocut  28423  halfcut  28458  addhalfcut  28459  bdaypw2n0bndlem  28463  bdayfinbndcbv  28466  bdayfinbndlem1  28467  bdayfinbndlem2  28468  z12bdaylem1  28470  elreno  28491  elreno2  28495  tgjustc1  28551  tgjustc2  28552  iscgrglt  28590  tgcgr4  28607  hlcgreu  28694  lmif  28861  islmib  28863  trgcopyeu  28882  iscgrad  28887  inaghl  28921  axlowdim2  29037  axlowdim  29038  axcontlem2  29042  axcontlem3  29043  axcontlem4  29044  axcontlem7  29047  axcontlem9  29049  axcontlem10  29050  axcontlem11  29051  axcontlem12  29052  ebtwntg  29059  umgrupgr  29180  nbusgrvtxm1  29456  crctcshwlkn0lem2  29888  crctcshwlkn0lem3  29889  crctcsh  29901  wlkswwlksf1o  29956  clwlkclwwlklem2fv1  30074  clwlkclwwlkf  30087  0clwlkv  30210  eupth2  30318  numclwwlk5  30467  nmoubi  30851  minvecolem2  30954  minvecolem3  30955  minvecolem4c  30958  minvecolem4  30959  minvecolem5  30960  minvecolem6  30961  htthlem  30996  chlimi  31313  chcompl  31321  hsn0elch  31327  cmbr3  31687  cmcm  31693  cmcm3  31694  lecm  31696  nmopub  31987  nmfnleub  32004  nmopun  32093  nmcexi  32105  cnlnadjlem7  32152  pjnmopi  32227  stle0i  32318  stlesi  32320  stm1i  32322  csmdsymi  32413  cvmd  32415  atcveq0  32427  atcv1  32459  atord  32467  atcvat2  32468  chirred  32474  mdsym  32491  mddmdin0i  32510  cdj1i  32512  fmptcof2  32738  fnpreimac  32751  isoun  32783  fcobijfs  32802  fcobijfs2  32803  lt2addrd  32832  xlt2addrd  32841  xrge0infss  32842  infxrge0glb  32847  xrofsup  32849  fz1nnct  32883  sgnmulsgn  32925  toslublem  33056  tosglblem  33058  ismntd  33068  mgccole1  33074  mgccole2  33075  mgcmnt1  33076  mgcmnt2  33077  dfmgc2lem  33079  dfmgc2  33080  psgnfzto1stlem  33184  fzto1st  33187  psgnfzto1st  33189  trsp2cyc  33207  xrnarchi  33268  archirng  33272  archiexdiv  33274  archiabl  33282  isarchiofld  33283  elrgspnlem1  33326  elrgspnlem2  33327  elrgspnlem3  33328  elrgspnlem4  33329  elrgspn  33330  elrgspnsubrunlem1  33331  elrgspnsubrunlem2  33332  elrgspnsubrun  33333  linds2eq  33464  elrspunidl  33511  elrspunsn  33512  isrprm  33600  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  extvfvvcl  33702  extvfvcl  33703  mplmulmvr  33706  evlextv  33709  mplvrpmlem  33710  mplvrpmfgalem  33711  mplvrpmga  33712  mplvrpmmhm  33713  mplvrpmrhm  33714  esplyfval0  33724  esplylem  33726  esplyfv1  33729  esplyfval3  33732  esplyind  33733  ply1degltdimlem  33781  lbsdiflsp0  33785  fedgmullem1  33788  fedgmullem2  33789  fedgmul  33790  fldextrspunlsplem  33832  fldextrspunlsp  33833  smatrcl  33955  smatlem  33956  madjusmdetlem2  33987  madjusmdet  33990  cmpcref  34009  ldlfcntref  34013  dispcmp  34018  zarcmplem  34040  ordtrest2NEWlem  34081  ordtconnlem1  34083  xrge0iifiso  34094  rge0scvg  34108  gsumesum  34218  esumfsup  34229  esumpinfval  34232  esumpcvgval  34237  esumcvg  34245  sigaclcu  34276  sigaclci  34291  unelsiga  34293  unelldsys  34317  sigapildsys  34321  ldgenpisyslem1  34322  fiunelros  34333  measvun  34368  voliune  34388  volfiniune  34389  oms0  34456  omssubaddlem  34458  omssubadd  34459  carsgsigalem  34474  carsgclctunlem2  34478  carsgclctun  34480  pmeasmono  34483  pmeasadd  34484  orvcval2  34618  dstfrvel  34633  ballotlemfc0  34652  ballotlemfcc  34653  ballotlemsv  34669  ballotlemsf1o  34673  breprexp  34792  tgoldbachgt  34822  bnj23  34876  bnj1185  34951  bnj1152  35156  bnj1418  35198  fnrelpredd  35249  loop1cycl  35333  umgr2cycl  35337  acycgrcycl  35343  dfdm5  35969  dfrn5  35970  wzel  36018  wsuclem  36019  brpprod  36079  brsset  36083  brbigcup  36092  dffix2  36099  elfuns  36109  brimageg  36121  brdomaing  36129  brrangeg  36130  brimg  36131  brapply  36132  lemsuccf  36135  funpartlem  36138  brrestrict  36145  dfrecs2  36146  dfrdg4  36147  brofs  36201  btwncomim  36209  btwnintr  36215  btwnexch3  36216  btwnexch2  36219  brifs  36239  brcolinear2  36254  colineardim1  36257  brfs  36275  btwnconn1  36297  segcon2  36301  seglerflx  36308  seglemin  36309  btwnsegle  36313  colinbtwnle  36314  broutsideof2  36318  fvray  36337  lineunray  36343  lineelsb2  36344  linerflx1  36345  trer  36512  elicc3  36513  finminlem  36514  nn0prpwlem  36518  nn0prpw  36519  fnessref  36553  refssfne  36554  weiunlem  36659  weiunfrlem  36660  weiunfr  36663  weiunse  36664  unblimceq0lem  36708  unblimceq0  36709  unbdqndv2  36713  knoppndvlem21  36734  taupilemrplb  37527  dfgcd3  37531  icorempo  37558  icoreval  37560  iooelexlt  37569  relowlssretop  37570  domalom  37611  ctbssinf  37613  pibt2  37624  phpreu  37807  fin2solem  37809  fin2so  37810  ltflcei  37811  ptrecube  37823  poimirlem1  37824  poimirlem2  37825  poimirlem5  37828  poimirlem6  37829  poimirlem7  37830  poimirlem9  37832  poimirlem12  37835  poimirlem22  37845  poimirlem23  37846  poimirlem24  37847  poimirlem26  37849  poimirlem27  37850  poimirlem32  37855  heicant  37858  mblfinlem1  37860  mblfinlem2  37861  itg2addnclem  37874  itg2addnclem3  37876  itg2addnc  37877  itg2gt0cn  37878  ibladdnclem  37879  iblmulc2nc  37888  itgabsnc  37892  ftc1anclem5  37900  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  indexdom  37937  filbcmb  37943  fdc  37948  prdsbnd  37996  heiborlem3  38016  rrnequiv  38038  rngoueqz  38143  eqbrtr  38441  elrnressn  38483  inxprnres  38501  presucmap  38698  eqvreltr  38894  prtlem10  39193  lsatcveq0  39360  lsatcv1  39376  oposlem  39510  opnlen0  39516  lub0N  39517  glb0N  39521  omllaw  39571  cmtbr4N  39583  cvrval  39597  cvrnbtwn  39599  cvrnbtwn2  39603  cvrnbtwn3  39604  cvrcon3b  39605  cvrnbtwn4  39607  atcvreq0  39642  atnle  39645  atlatmstc  39647  cvlexch1  39656  glbconN  39705  hlsuprexch  39709  exatleN  39732  cvratlem  39749  atcvrj0  39756  atcvrj2b  39760  atlelt  39766  cvrat4  39771  3dim1lem5  39794  3dim2  39796  3dim3  39797  ps-2  39806  llni  39836  llnn0  39844  llnle  39846  lplni  39860  lplni2  39865  lplnle  39868  lplnn0N  39875  llncvrlpln  39886  2llnjN  39895  lvoli  39903  lvoli3  39905  lvoli2  39909  lvoln0N  39919  4at  39941  lplncvrlvol  39944  2lplnj  39948  dalemcea  39988  dalem3  39992  psubspi  40075  linepsubN  40080  elpmap  40086  pmapsub  40096  lnatexN  40107  cdlema1N  40119  cdlemb  40122  elpadd  40127  paddvaln0N  40129  paddasslem5  40152  llnexchb2lem  40196  llnexch2N  40198  islhp  40324  lhpat3  40374  4atexlemex2  40399  4atex  40404  4atex2-0aOLDN  40406  4atex2-0cOLDN  40408  lautle  40412  lautcvr  40420  lauteq  40423  ldilval  40441  ltrnu  40449  trlval2  40491  trlne  40513  cdleme0ex1N  40551  cdleme0nex  40618  cdleme18d  40623  cdlemednuN  40628  cdleme25b  40682  cdleme25cv  40686  cdleme27b  40696  cdleme29b  40703  cdleme31sn  40708  cdleme31fv  40718  cdleme31fv2  40721  cdlemefrs29bpre0  40724  cdlemefr29bpre0N  40734  cdlemefr29clN  40735  cdlemefr32fvaN  40737  cdlemefr32fva1  40738  cdlemefs29pre00N  40740  cdlemefs32sn1aw  40742  cdlemefs29bpre0N  40744  cdlemefs29bpre1N  40745  cdlemefs29cpre1N  40746  cdlemefs29clN  40747  cdlemefs32fvaN  40750  cdlemefs32fva1  40751  cdleme41sn3a  40761  cdleme32fva  40765  cdleme32e  40773  cdleme35f  40782  cdleme40v  40797  cdleme42b  40806  trlord  40897  cdlemg1cex  40916  diaval  41360  diaeldm  41364  diaelrnN  41373  cdlemm10N  41446  dibglbN  41494  dicval  41504  dicfnN  41511  dicvalrelN  41513  dihval  41560  dihlsscpre  41562  dihglblem3N  41623  dihmeetlem2N  41627  djhcvat42  41743  lcmineqlem4  42354  aks4d1p4  42401  aks4d1p5  42402  aks4d1p7  42405  aks4d1p8d2  42407  aks4d1p8  42409  hashnexinjle  42451  sticksstones1  42468  sticksstones2  42469  sticksstones10  42477  sticksstones12a  42479  aks6d1c7lem4  42505  aks6d1c7  42506  grpods  42516  unitscyglem2  42518  unitscyglem3  42519  unitscyglem4  42520  qsalrel  42563  supinf  42564  dvdsexpnn0  42656  redvmptabs  42682  sn-nnne0  42782  sn-sup2  42813  fimgmcyclem  42855  flt4lem2  42957  flt4lem7  42969  lzenom  43079  fphpdo  43126  irrapxlem4  43134  pellexlem6  43143  infmrgelbi  43187  pellfundre  43190  pellfundlb  43193  monotoddzz  43252  zindbi  43255  jm2.27  43317  rmydioph  43323  rpnnen3lem  43340  fnwe2lem2  43360  aomclem8  43370  hbtlem5  43437  hbt  43439  sdomne0  43721  sdomne0d  43722  ensucne0  43837  sucomisnotcard  43852  en2pr  43855  pr2cv  43856  refimssco  43915  rfovfvfvd  44311  rfovcnvf1od  44312  fsovrfovd  44317  nzss  44625  relprel  45259  permaxinf2lem  45320  wessf1ornlem  45496  axccdom  45533  dmrelrnrel  45537  axccd  45540  rnmptlb  45554  rnmptbdd  45556  rnmptbd2  45560  rnmptbdlem  45566  rnmptbd  45567  dstregt0  45597  suplesup  45651  supxrunb3  45710  supxrleubrnmpt  45717  rexabslelem  45729  rexabsle  45730  suprleubrnmpt  45733  infrnmptle  45734  infxrunb3rnmpt  45739  infxrpnf  45757  supminfxr  45775  infrpgernmpt  45776  xrpnf  45796  limsupre  45952  limsupref  45996  limsupbnd1f  45997  limsuppnfd  46013  climinf2  46018  limsuppnf  46022  climinfmpt  46026  climinf3  46027  limsupmnflem  46031  limsupmnf  46032  limsupre2  46036  limsupmnfuzlem  46037  limsupre2mpt  46041  limsupre3lem  46043  limsupre3  46044  limsupre3mpt  46045  limsupre3uzlem  46046  limsupre3uz  46047  limsupreuz  46048  limsupreuzmpt  46050  liminfval2  46079  liminfreuzlem  46113  liminfreuz  46114  xlimpnfxnegmnf  46125  cnrefiisplem  46140  xlimpnfv  46149  xlimpnf  46153  xlimpnfmpt  46155  dfxlim2  46159  icccncfext  46198  cncficcgt0  46199  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  stoweidlem5  46316  stoweidlem20  46331  stoweidlem26  46337  stoweidlem28  46339  stoweidlem29  46340  stoweidlem34  46345  wallispilem3  46378  stirlinglem13  46397  fourierdlem41  46459  fourierdlem42  46460  fourierdlem51  46468  fourierdlem54  46471  salunicl  46627  saluncl  46628  salexct  46645  salexct2  46650  salexct3  46653  salgencntex  46654  salgensscntex  46655  sge0pnffigt  46707  meadjuni  46768  omeunile  46816  ovnlerp  46873  hoidifhspval  46919  ovolval5lem2  46964  salpreimagelt  47018  pimincfltioo  47029  salpreimagtge  47036  salpreimagtlt  47041  incsmf  47053  issmfgt  47067  smfpreimagt  47073  decsmf  47078  issmfge  47081  smfpimgtxr  47091  smfpreimage  47093  smfinflem  47128  smfinf  47129  finfdm  47157  funressnfv  47356  funressnvmo  47358  funressnmo  47359  dfdfat2  47441  tz6.12-afv  47486  funressndmafv2rn  47536  tz6.12-afv2  47553  dfatcolem  47568  dfatco  47569  zplusmodne  47656  m1modne  47661  minusmod5ne  47662  submodneaddmod  47664  modmknepk  47675  iccpartigtl  47736  iccpartgt  47740  icceuelpartlem  47748  iccpartnel  47751  sprsymrelfolem2  47806  goldbachthlem2  47859  odz2prm2pw  47876  fmtnoprmfac1  47878  fmtnoprmfac2  47880  fmtnofac2  47882  fmtno4prmfac  47885  fmtno4prm  47888  prmdvdsfmtnof1lem1  47897  31prm  47910  perfectALTVlem2  48035  nnsum3primes4  48101  nnsum3primesprm  48103  nnsum3primesgbe  48105  nnsum3primesle9  48107  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  wtgoldbnnsum4prm  48115  bgoldbnnsum3prm  48117  bgoldbtbndlem4  48121  bgoldbtbnd  48122  tgblthelfgott  48128  tgoldbach  48130  assintop  48522  isassintop  48523  assintopcllaw  48525  ztprmneprm  48660  ply1mulgsumlem1  48699  ply1mulgsumlem2  48700  lco0  48740  lcoel0  48741  lincsumcl  48744  lincscmcl  48745  lcoss  48749  linindslinci  48761  lindslinindsimp1  48770  linds0  48778  el0ldep  48779  lindsrng01  48781  ldepspr  48786  islindeps2  48796  isldepslvec2  48798  zlmodzxzldep  48817  ldepsnlinc  48821  elbigo2r  48866  xpco2  49169  tposres0  49189  lubsscl  49272  glbsscl  49273  lubprlem  49274  ipolub  49300  ipoglb  49303  catprslem  49322  infsubc2  49373  nelsubc3lem  49382  cnelsubclem  49915  setrec2lem1  50005