Theorem breq1 5105

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144  ⟨cop 4590   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  breq12  5107  breq1i  5109  breq1d  5112  nbrne2  5122  brab1  5150  pocl  5565  swopolem  5567  swopo  5568  po2ne  5573  solin  5584  sotrieq  5588  sotr2  5591  isso2i  5594  somo  5596  dffr2  5610  frc  5612  frirr  5625  fr2nr  5626  wereu2  5646  vtoclr  5712  frsn  5737  brcog  5840  brcogw  5842  brcnvg  5853  dfdmf  5874  eldmg  5876  dmun  5888  dm0rn0  5902  dfrnf  5928  dmcosseq  5956  dmcosseqOLD  5957  dfres2  6032  imasng  6075  cotrg  6100  cnvsym  6103  asymref2  6106  sotri2  6118  somin1  6122  rnco  6241  coi1  6252  predtrss  6311  frpomin  6329  dffun2  6533  dffun6f  6538  funmo  6539  fun11  6597  fveq2  6869  eliman0  6906  nfunsn  6908  dffv2  6964  fvopab5  7011  dff3  7083  f1ompt  7094  fmptco  7113  dff13  7240  foeqcnvco  7286  isorel  7312  soisores  7313  soisoi  7314  isocnv  7316  isotr  7322  isomin  7323  isoini  7324  isopolem  7331  isosolem  7333  f1oiso  7337  f1oiso2  7338  weniso  7340  eqfunresadj  7346  caovordig  7603  caovordg  7605  caovord3d  7608  caovord  7609  caovord3  7611  caofrss  7701  caoftrn  7703  fr3nr  7757  dfwe2  7759  f1oweALT  7955  frxp  8108  poxp  8110  fnse  8115  poxp2  8125  frxp2  8126  poxp3  8132  frxp3  8133  xpord3pred  8134  poseq  8140  brtpos2  8214  rntpos  8221  tpostpos  8228  frrlem12  8280  ertr  8696  ecopovsym  8803  ecopovtrn  8804  isfi  8958  en0  9001  en0ALT  9002  en1  9007  endisj  9038  xpcomco  9041  sbth  9071  2pwne  9107  disjenex  9109  ssenen  9125  findcard  9134  findcard2  9135  pssnn  9139  sbthfi  9169  nneneq  9176  php  9177  onomeneq  9184  sdom1  9196  1sdom2dom  9200  isinf  9211  fineqvlem  9212  en1eqsnbi  9222  findcard3  9229  frfi  9231  fiint  9273  mapfienlem1  9353  mapfienlem2  9354  mapfienlem3  9355  mapfien  9356  marypha1lem  9381  supmo  9400  eqsup  9404  supub  9407  suplub  9408  suppr  9420  supisolem  9422  supisoex  9423  infmin  9444  infmo  9445  fiinfg  9449  fiinf2g  9450  infpr  9453  ordtypecbv  9467  ordtypelem3  9470  ordtypelem6  9473  ordtypelem7  9474  ordtypelem9  9476  ordtypelem10  9477  hartogslem1  9492  hartogs  9494  wemaplem1  9496  wemaplem2  9497  wemapso2lem  9502  card2on  9504  card2inf  9505  elharval  9511  brwdom2  9523  wdomtr  9525  cantnfs  9623  cantnfp1lem2  9636  oemapso  9639  cantnflem1  9646  wemapwe  9654  ttrclss  9677  r111  9735  kardex  9854  karden  9855  isnumi  9906  tskwe  9910  cardid2  9913  cardonle  9917  cardne  9925  iscard2  9936  infxpenlem  9971  fodomfi2  10018  wdomfil  10019  wdomnumr  10022  alephsuc2  10038  infenaleph  10049  iunfictbso  10072  infpss  10174  cff1  10217  cfslb2n  10227  sornom  10236  fin4i  10257  isfin6  10259  isfin7  10260  isfin1-3  10345  fin1a2lem9  10367  fin1a2lem11  10369  hsmexlem4  10388  axcc2lem  10395  axcc4dom  10400  domtriomlem  10401  numthcor  10453  zorn2lem2  10456  zorn2lem3  10457  zorn2lem7  10461  zorn2g  10462  axdclem  10478  axdc  10480  brdom7disj  10490  brdom6disj  10491  uniimadom  10503  ondomon  10522  alephval2  10532  alephreg  10542  pwcfsdom  10543  elgch  10582  gchi  10584  fpwwe2lem11  10601  fpwwe2lem12  10602  winainflem  10653  winalim2  10656  tsken  10714  0tsk  10715  inar1  10735  tskord  10740  tskuni  10743  grudomon  10777  pinq  10887  nqereu  10889  enqeq  10894  ltbtwnnq  10938  ltrnq  10939  prcdnq  10953  prnmax  10955  genpnmax  10967  nqpr  10974  1idpr  10989  reclem2pr  11008  reclem3pr  11009  reclem4pr  11010  recexpr  11011  supexpr  11014  ltsosr  11054  1ne0sr  11056  ltasr  11060  supsrlem  11071  axpre-lttri  11125  axpre-lttrn  11126  axpre-ltadd  11127  axpre-sup  11129  lelttr  11275  dedekind  11348  dedekindle  11349  ltordlem  11714  lt0ne0d  11754  fimaxre3  12140  fiminre2  12142  lbreu  12144  lble  12146  sup2  12150  infm3  12153  suprleub  12160  supaddc  12161  supadd  12162  supmul1  12163  supmullem1  12164  supmul  12166  nnne0  12249  nnsub  12259  nominpos  12460  nnunb  12479  arch  12480  nn0sub  12533  nn0n0n1ge2b  12552  nn0lt10b  12637  zextle  12648  peano5uzti  12665  fzind  12673  btwnz  12678  uzval  12843  uzwo  12914  nnwof  12917  ublbneg  12936  lbzbi  12939  zsupss  12940  uzsupss  12943  uzwo3  12946  zmax  12948  rebtwnz  12950  rpnnen1lem3  12982  xrltnsym  13141  xrlttri  13143  xrlttr  13144  xrlelttr  13160  nltpnft  13169  xrmaxlt  13186  xrmaxle  13188  qbtwnre  13204  qbtwnxr  13205  xltnegi  13221  xnn0lenn0nn0  13250  xsubge0  13266  xlesubadd  13268  xmullem2  13270  xlemul1a  13293  xrinfmexpnf  13311  xrsupsslem  13312  xrinfmsslem  13313  xrub  13317  supxrunb1  13324  supxrunb2  13325  reltre  13346  rpltrp  13347  reltxrnmnf  13348  ixxval  13359  elixx1  13360  elioo2  13392  iccid  13396  icc0  13399  fzval  13516  elfz1  13519  elfznelfzo  13781  elfznelfzob  13782  flval  13806  fllelt  13809  flflp1  13819  flval2  13826  flval3  13827  flbi  13828  dfceil2  13851  ceilval2  13852  fleqceilz  13866  modid2  13910  addmodlteq  13961  fsequb2  13991  ssnn0fi  14000  seqf1olem2  14057  sqlecan  14224  faclbnd4lem1  14308  hashsnle1  14432  pr2pwpr  14494  hash3tpde  14508  rtrclreclem3  15075  relexpindlem  15078  sgnval  15103  sgnmulsgn  15124  01sqrexlem6  15276  01sqrex  15278  abslt  15344  absle  15345  rexanre  15376  rexico  15383  limsupgle  15506  limsupgre  15510  limsupbnd2  15512  rlim2lt  15526  rlim3  15527  ello12r  15546  ello1d  15552  elo12r  15557  rlimconst  15573  climshft  15605  rlimcn3  15619  o1rlimmul  15648  lo1le  15681  climsup  15699  caucvgrlem  15702  isumless  15877  divrcnv  15884  cvgrat  15915  rpnnen2lem10  16257  ruclem1  16265  ruclem2  16266  ruclem11  16274  ruclem12  16275  sqrt2irr  16283  absdvdsb  16310  dvdsle  16346  dvdsabseq  16349  dvdsdivcl  16352  dvdsext  16357  divalglem8  16436  divalglem9  16437  divalglem10  16438  divalgmod  16442  ndvdssub  16445  sadcaddlem  16493  gcdcllem1  16535  gcdcllem2  16536  gcdcllem3  16537  dfgcd2  16582  gcdzeq  16588  dvdssq  16603  nn0seqcvgd  16606  algcvgblem  16613  lcmval  16628  lcmdvds  16644  lcmgcdeq  16648  lcmfpr  16663  lcmf  16669  lcmftp  16672  lcmfunsnlem1  16673  lcmfunsnlem2lem1  16674  lcmfunsnlem2lem2  16675  lcmfdvdsb  16679  coprmgcdb  16685  coprmdvds1  16688  1nprm  16715  1idssfct  16716  isprm2lem  16717  isprm2  16718  dvdsprime  16723  nprm  16724  3prm  16730  dvdsprm  16740  exprmfct  16741  isprm5  16744  maxprmfct  16746  coprm  16748  prmdvdsncoprmbd  16764  ncoprmlnprm  16765  eulerthlem2  16819  phisum  16828  odzval  16829  pythagtriplem4  16857  pc2dvds  16917  pcprmpw2  16920  pcprmpw  16921  dvdsprmpweqle  16924  oddprmdvds  16941  prmpwdvds  16942  pockthg  16944  unbenlem  16946  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  1arith  16965  vdwlem6  17024  vdwlem11  17029  vdwlem13  17031  ramtlecl  17038  ramub  17051  rami  17053  ramubcl  17056  0ram  17058  ram0  17060  prmdvdsprmop  17081  prmolefac  17084  prmodvdslcmf  17085  prmgaplem2  17088  prmgaplcmlem1  17089  prmgaplcmlem2  17090  prmgaplem3  17091  prmgaplem4  17092  prmgaplem5  17093  prmgaplem6  17094  prmgapprmolem  17099  prmlem0  17143  prmlem1a  17144  imasaddfnlem  17560  imasvscafn  17569  imasleval  17573  prslem  18331  drsdir  18336  drsdirfi  18339  isdrs2  18340  posi  18351  posasymb  18353  pospropd  18359  pltval3  18371  plelttr  18376  pospo  18377  lubprop  18390  luble  18391  lublecllem  18392  glbprop  18403  joinval2lem  18412  joinlem  18415  meetlem  18429  meetle  18432  poslubmo  18443  posglbmo  18444  poslubd  18445  tleile  18453  latnlej  18490  isglbd  18543  lubub  18545  lubun  18549  clatleglb  18552  tsrlin  18619  letsr  18627  dirge  18637  pmtrval  19493  pmtrrn  19499  pmtrfrn  19500  pmtrrn2  19502  pmtrsn  19561  mndodcongi  19585  odeq  19592  odmulgeq  19599  gexnnod  19630  sylow1lem1  19640  pgpssslw  19656  sylow2a  19661  efgredeu  19794  efgred2  19795  gexex  19895  frgpnabllem2  19916  cyggenod  19926  dprdval  20047  dprdw  20054  dprdwd  20055  ablfacrplem  20109  ablfac1c  20115  ablfac1eu  20117  ablfaclem3  20131  omndadd  20170  abvtrivd  20883  zringlpir  21521  prmirredlem  21526  znleval  21608  frlmelbas  21810  ellspd  21856  islindf4  21892  psrbagconcl  21981  psrbagleadd1  21982  gsumbagdiaglem  21985  rhmpsrlem2  21995  psrlidm  22015  psrridm  22016  psrass1  22017  psrcom  22021  mplelbas  22044  mplmonmul  22091  ltbwe  22099  mhpmulcl  22216  psdmul  22233  coe1fsupp  22278  coe1ae0  22280  coe1mul2  22334  coe1tmmul  22342  pmatcoe1fsupp  22763  chfacffsupp  22918  chfacfscmulfsupp  22921  chfacfscmulgsum  22922  chfacfpmmulfsupp  22925  chfacfpmmulgsum  22926  ordtbas2  23253  ordtopn2  23257  ordtrest2lem  23265  pnfnei  23282  ordtt1  23441  ordthauslem  23445  2ndci  23510  2ndcsb  23511  2ndcredom  23512  2ndc1stc  23513  1stcrest  23515  2ndcctbss  23517  2ndcdisj  23518  2ndcsep  23521  lly1stc  23558  tx1stc  23712  ordthmeolem  23863  ufildom1  23988  xmetrtri2  24418  prdsxmetlem  24430  ssblex  24490  prdsbl  24553  comet  24575  stdbdxmet  24577  stdbdmopn  24580  met1stc  24583  dscmet  24634  metdstri  24914  metdscn  24919  xrhmeo  25010  bndth  25022  evth  25023  lebnumlem3  25027  pcovalg  25076  pco1  25079  pcocn  25081  pcopt  25086  pcopt2  25087  pcoass  25088  nmoleub3  25183  bcthlem5  25392  rrxfsupp  25466  minveclem4c  25489  minveclem2  25490  minveclem3b  25492  minveclem4  25496  minveclem6  25498  pmltpclem1  25512  pmltpc  25514  ovollb2lem  25552  ovolctb  25554  ovolunlem1  25561  ovoliunlem1  25566  ovoliunlem2  25567  ovoliun2  25570  ovolshftlem1  25573  ovolscalem1  25577  ovolicc1  25580  ovolicc2lem3  25583  voliunlem2  25615  voliunlem3  25616  ioombl1lem4  25625  uniioovol  25643  uniioombllem2  25647  uniioombllem3  25649  uniioombllem6  25652  volsup2  25669  ismbfd  25703  mbfsup  25728  mbflimsup  25730  itg1climres  25778  mbfi1fseqlem4  25782  itg2lr  25794  itg2leub  25798  itg2seq  25806  itg2monolem1  25814  itg2monolem3  25816  itg2mono  25817  itg2i1fseq2  25820  itg2gt0  25824  itg2cnlem1  25825  itg2cnlem2  25826  itg2cn  25827  iblss  25869  itgless  25881  ibladdlem  25884  iblabsr  25894  iblmulc2  25895  itgabs  25899  bddiblnc  25906  ditgeq1  25912  dvferm2lem  26050  rolle  26054  dvlip2  26059  c1liplem1  26060  c1lip1  26061  dvfsumlem2  26091  dvfsumlem4  26093  mdegleb  26126  degltlem1  26134  plyco0  26254  plyeq0lem  26272  coeeq2  26304  dgrle  26305  dgradd2  26330  plydiveu  26364  aareccl  26392  aalioulem2  26399  aaliou3lem7  26415  psercnlem1  26490  pilem2  26517  pilem3  26518  logltb  26667  divlogrlim  26702  logcnlem3  26711  cxpaddlelem  26818  rlimcnp  27032  cxplim  27038  cxploglim  27044  scvxcvx  27052  ftalem1  27139  ftalem2  27140  isppw2  27181  vmappw  27182  sgmnncl  27213  sqff1o  27248  fsumdvdsdiaglem  27249  dvdsppwf1o  27252  dvdsflsumcom  27254  musum  27257  muinv  27259  mpodvdsmulf1o  27260  dvdsmulf1o  27262  vmalelog  27271  vmasum  27282  logfac2  27283  perfectlem2  27296  bcmono  27343  bpos1lem  27348  bposlem9  27358  lgsmod  27389  lgsne0  27401  gausslemma2dlem4  27435  2sqlem6  27489  2sqlem8  27492  2sqlem10  27494  2sqreulem1  27512  2sqreunnlem1  27515  chtppilim  27541  rpvmasumlem  27553  dchrisumlema  27554  dchrisumlem2  27556  dchrvmasumlem1  27561  dchrvmasumiflem1  27567  dchrisum0flblem1  27574  dchrisum0flblem2  27575  dchrisum0  27586  rplogsum  27593  logsqvma  27608  pntpbnd1  27652  pntpbnd2  27653  pntibndlem3  27658  pntlemj  27669  pntlemi  27670  pntlem3  27675  pnt3  27678  ostth3  27704  nodense  27758  noresle  27763  nosupprefixmo  27766  noinfprefixmo  27767  nosupcbv  27768  nosupdm  27770  nosupbnd1lem1  27774  nosupbnd1lem4  27777  nosupbnd1  27780  nosupbnd2lem1  27781  nosupbnd2  27782  noinfcbv  27783  noinfdm  27785  noinffv  27787  noinfres  27788  noinfbnd1lem3  27791  noinfbnd1lem4  27792  noinfbnd1lem5  27793  noinfbnd1  27795  noetalem2  27808  nocvxminlem  27849  sltssnb  27864  sltssepc  27866  conway  27874  cutsval  27875  etaslts  27888  lesrec  27894  eqcuts3  27899  bday1  27909  cuteq1  27912  madeval2  27928  rightval  27945  elleft  27946  sltsright  27956  made0  27958  madecut  27978  left1s  27990  madebdaylemlrcut  27994  ltslpss  28003  cofslts  28013  coinitslts  28014  cofcutr  28019  cofcutrtime  28022  cofss  28025  coiniss  28026  cutmax  28029  cutmin  28030  cutminmax  28031  addsproplem1  28064  addsprop  28071  leadds1  28084  addsuniflem  28096  negsproplem1  28123  negsprop  28130  negsid  28136  negsunif  28150  mulsproplemcbv  28210  mulsproplem1  28211  mulsproplem9  28219  mulsprop  28225  sltmuls1  28242  sltmuls2  28243  mulsuniflem  28244  precsexlem11  28312  abslts  28344  oncutlt  28359  oniso  28366  bdayons  28371  addonbday  28374  n0fincut  28450  onsfi  28451  n0subs  28458  bdayn0p1  28464  eucliddivs  28471  zcuts  28502  twocut  28518  halfcut  28553  addhalfcut  28554  bdaypw2n0bndlem  28558  bdayfinbndcbv  28561  bdayfinbndlem1  28562  bdayfinbndlem2  28563  z12bdaylem1  28565  elreno  28586  elreno2  28590  tgjustc1  28646  tgjustc2  28647  iscgrglt  28685  tgcgr4  28702  hlcgreu  28789  lmif  28960  islmib  28962  trgcopyeu  28981  elplng  28989  plngcplem  28994  iscgrad  29007  inaghl  29041  axlowdim2  29163  axlowdim  29164  axcontlem2  29168  axcontlem3  29169  axcontlem4  29170  axcontlem7  29173  axcontlem9  29175  axcontlem10  29176  axcontlem11  29177  axcontlem12  29178  ebtwntg  29185  umgrupgr  29306  nbusgrvtxm1  29582  crctcshwlkn0lem2  30013  crctcshwlkn0lem3  30014  crctcsh  30026  wlkswwlksf1o  30081  clwlkclwwlklem2fv1  30199  clwlkclwwlkf  30212  0clwlkv  30335  eupth2  30443  numclwwlk5  30592  nmoubi  30977  minvecolem2  31080  minvecolem3  31081  minvecolem4c  31084  minvecolem4  31085  minvecolem5  31086  minvecolem6  31087  htthlem  31122  chlimi  31439  chcompl  31447  hsn0elch  31453  cmbr3  31813  cmcm  31819  cmcm3  31820  lecm  31822  nmopub  32113  nmfnleub  32130  nmopun  32219  nmcexi  32231  cnlnadjlem7  32278  pjnmopi  32353  stle0i  32444  stlesi  32446  stm1i  32448  csmdsymi  32539  cvmd  32541  atcveq0  32553  atcv1  32585  atord  32593  atcvat2  32594  chirred  32600  mdsym  32617  mddmdin0i  32636  cdj1i  32638  fmptcof2  32861  fnpreimac  32874  isoun  32906  fcobijfs  32925  fcobijfs2  32926  lt2addrd  32954  xlt2addrd  32963  xrge0infss  32964  infxrge0glb  32969  xrofsup  32971  fz1nnct  33005  toslublem  33152  tosglblem  33154  ismntd  33164  mgccole1  33170  mgccole2  33171  mgcmnt1  33172  mgcmnt2  33173  dfmgc2lem  33175  dfmgc2  33176  psgnfzto1stlem  33282  fzto1st  33285  psgnfzto1st  33287  trsp2cyc  33305  xrnarchi  33366  archirng  33370  archiexdiv  33372  archiabl  33380  isarchiofld  33381  elrgspnlem1  33425  elrgspnlem2  33426  elrgspnlem3  33427  elrgspnlem4  33428  elrgspn  33429  elrgspnsubrunlem1  33430  elrgspnsubrunlem2  33431  elrgspnsubrun  33432  linds2eq  33569  elrspunidl  33616  elrspunsn  33617  isrprm  33715  evl1deg1  33774  evl1deg2  33775  evl1deg3  33776  0mplrim  33813  selvply1rhmlema  33817  selvply1rhmlemb  33818  selvply1rhmlem1  33819  selvply1rhmlem2  33820  selvply1rhmlem4  33822  selvply1rhm0  33825  extvfvvcl  33834  extvfvcl  33835  mplmulmvr  33838  evlextv  33841  mplvrpmlem  33842  mplvrpmfgalem  33843  mplvrpmga  33844  mplvrpmmhm  33845  mplvrpmrhm  33846  psrmonmul  33849  psrmonprod  33851  esplyfval0  33863  esplylem  33865  esplyfv1  33868  esplyfval3  33871  esplyfvaln  33873  esplyind  33874  ply1degltdimlem  33921  lbsdiflsp0  33925  fedgmullem1  33928  fedgmullem2  33929  fedgmul  33930  fldextrspunlsplem  33972  fldextrspunlsp  33973  smatrcl  34095  smatlem  34096  madjusmdetlem2  34127  madjusmdet  34130  cmpcref  34149  ldlfcntref  34153  dispcmp  34158  zarcmplem  34180  ordtrest2NEWlem  34221  ordtconnlem1  34223  xrge0iifiso  34234  rge0scvg  34248  gsumesum  34358  esumfsup  34369  esumpinfval  34372  esumpcvgval  34377  esumcvg  34385  sigaclcu  34416  sigaclci  34431  unelsiga  34433  unelldsys  34457  sigapildsys  34461  ldgenpisyslem1  34462  fiunelros  34473  measvun  34508  voliune  34528  volfiniune  34529  oms0  34596  omssubaddlem  34598  omssubadd  34599  carsgsigalem  34614  carsgclctunlem2  34618  carsgclctun  34620  pmeasmono  34623  pmeasadd  34624  orvcval2  34758  dstfrvel  34773  ballotlemfc0  34792  ballotlemfcc  34793  ballotlemsv  34809  ballotlemsf1o  34813  breprexp  34929  tgoldbachgt  34959  bnj23  35016  bnj1185  35090  bnj1152  35295  bnj1418  35337  fnrelpredd  35389  loop1cycl  35492  umgr2cycl  35496  acycgrcycl  35502  dfdm5  36128  dfrn5  36129  wzel  36177  wsuclem  36178  brpprod  36238  brsset  36242  brbigcup  36251  dffix2  36258  elfuns  36268  brimageg  36280  brdomaing  36288  brrangeg  36289  brimg  36290  brapply  36291  lemsuccf  36294  funpartlem  36297  brrestrict  36304  dfrecs2  36305  dfrdg4  36306  brofs  36360  btwncomim  36368  btwnintr  36374  btwnexch3  36375  btwnexch2  36378  brifs  36398  brcolinear2  36413  colineardim1  36416  brfs  36434  btwnconn1  36456  segcon2  36460  seglerflx  36467  seglemin  36468  btwnsegle  36472  colinbtwnle  36473  broutsideof2  36477  fvray  36496  lineunray  36502  lineelsb2  36503  linerflx1  36504  trer  36681  elicc3  36682  finminlem  36683  nn0prpwlem  36687  nn0prpw  36688  fnessref  36722  refssfne  36723  weiunlem  36828  weiunfrlem  36829  weiunfr  36832  weiunse  36833  unblimceq0lem  36949  unblimceq0  36950  unbdqndv2  36954  knoppndvlem21  36975  taupilemrplb  37817  dfgcd3  37821  icorempo  37850  icoreval  37852  iooelexlt  37861  relowlssretop  37862  domalom  37903  ctbssinf  37905  pibt2  37916  phpreu  38108  fin2solem  38110  fin2so  38111  ltflcei  38112  ptrecube  38124  poimirlem1  38125  poimirlem2  38126  poimirlem5  38129  poimirlem6  38130  poimirlem7  38131  poimirlem9  38133  poimirlem12  38136  poimirlem22  38146  poimirlem23  38147  poimirlem24  38148  poimirlem26  38150  poimirlem27  38151  poimirlem32  38156  heicant  38159  mblfinlem1  38161  mblfinlem2  38162  itg2addnclem  38175  itg2addnclem3  38177  itg2addnc  38178  itg2gt0cn  38179  ibladdnclem  38180  iblmulc2nc  38189  itgabsnc  38193  ftc1anclem5  38201  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  indexdom  38238  filbcmb  38244  fdc  38249  prdsbnd  38297  heiborlem3  38317  rrnequiv  38339  rngoueqz  38444  eqbrtr  38742  elrnressn  38784  inxprnres  38802  presucmap  38999  eqvreltr  39195  prtlem10  39494  lsatcveq0  39661  lsatcv1  39677  oposlem  39811  opnlen0  39817  lub0N  39818  glb0N  39822  omllaw  39872  cmtbr4N  39884  cvrval  39898  cvrnbtwn  39900  cvrnbtwn2  39904  cvrnbtwn3  39905  cvrcon3b  39906  cvrnbtwn4  39908  atcvreq0  39943  atnle  39946  atlatmstc  39948  cvlexch1  39957  glbconN  40006  hlsuprexch  40010  exatleN  40033  cvratlem  40050  atcvrj0  40057  atcvrj2b  40061  atlelt  40067  cvrat4  40072  3dim1lem5  40095  3dim2  40097  3dim3  40098  ps-2  40107  llni  40137  llnn0  40145  llnle  40147  lplni  40161  lplni2  40166  lplnle  40169  lplnn0N  40176  llncvrlpln  40187  2llnjN  40196  lvoli  40204  lvoli3  40206  lvoli2  40210  lvoln0N  40220  4at  40242  lplncvrlvol  40245  2lplnj  40249  dalemcea  40289  dalem3  40293  psubspi  40376  linepsubN  40381  elpmap  40387  pmapsub  40397  lnatexN  40408  cdlema1N  40420  cdlemb  40423  elpadd  40428  paddvaln0N  40430  paddasslem5  40453  llnexchb2lem  40497  llnexch2N  40499  islhp  40625  lhpat3  40675  4atexlemex2  40700  4atex  40705  4atex2-0aOLDN  40707  4atex2-0cOLDN  40709  lautle  40713  lautcvr  40721  lauteq  40724  ldilval  40742  ltrnu  40750  trlval2  40792  trlne  40814  cdleme0ex1N  40852  cdleme0nex  40919  cdleme18d  40924  cdlemednuN  40929  cdleme25b  40983  cdleme25cv  40987  cdleme27b  40997  cdleme29b  41004  cdleme31sn  41009  cdleme31fv  41019  cdleme31fv2  41022  cdlemefrs29bpre0  41025  cdlemefr29bpre0N  41035  cdlemefr29clN  41036  cdlemefr32fvaN  41038  cdlemefr32fva1  41039  cdlemefs29pre00N  41041  cdlemefs32sn1aw  41043  cdlemefs29bpre0N  41045  cdlemefs29bpre1N  41046  cdlemefs29cpre1N  41047  cdlemefs29clN  41048  cdlemefs32fvaN  41051  cdlemefs32fva1  41052  cdleme41sn3a  41062  cdleme32fva  41066  cdleme32e  41074  cdleme35f  41083  cdleme40v  41098  cdleme42b  41107  trlord  41198  cdlemg1cex  41217  diaval  41661  diaeldm  41665  diaelrnN  41674  cdlemm10N  41747  dibglbN  41795  dicval  41805  dicfnN  41812  dicvalrelN  41814  dihval  41861  dihlsscpre  41863  dihglblem3N  41924  dihmeetlem2N  41928  djhcvat42  42044  lcmineqlem4  42654  aks4d1p4  42701  aks4d1p5  42702  aks4d1p7  42705  aks4d1p8d2  42707  aks4d1p8  42709  hashnexinjle  42751  sticksstones1  42768  sticksstones2  42769  sticksstones10  42777  sticksstones12a  42779  aks6d1c7lem4  42805  aks6d1c7  42806  grpods  42816  unitscyglem2  42818  unitscyglem3  42819  unitscyglem4  42820  qsalrel  42862  supinf  42863  dvdsexpnn0  42948  redvmptabs  42974  sn-nnne0  43087  sn-sup2  43118  fimgmcyclem  43156  flt4lem2  43234  flt4lem7  43246  lzenom  43356  fphpdo  43399  irrapxlem4  43407  pellexlem6  43416  infmrgelbi  43460  pellfundre  43463  pellfundlb  43466  monotoddzz  43525  zindbi  43528  jm2.27  43590  rmydioph  43596  rpnnen3lem  43613  fnwe2lem2  43633  aomclem8  43643  hbtlem5  43710  hbt  43712  sdomne0  43994  sdomne0d  43995  ensucne0  44110  sucomisnotcard  44125  en2pr  44128  pr2cv  44129  refimssco  44188  rfovfvfvd  44584  rfovcnvf1od  44585  fsovrfovd  44590  nzss  44898  relprel  45532  permaxinf2lem  45593  wessf1ornlem  45768  axccdom  45803  dmrelrnrel  45807  axccd  45809  rnmptlb  45823  rnmptbdd  45825  rnmptbd2  45829  rnmptbdlem  45835  rnmptbd  45836  dstregt0  45866  suplesup  45920  supxrunb3  45979  supxrleubrnmpt  45985  rexabslelem  45997  rexabsle  45998  suprleubrnmpt  46001  infrnmptle  46002  infxrunb3rnmpt  46007  infxrpnf  46025  supminfxr  46043  infrpgernmpt  46044  xrpnf  46064  limsupre  46220  limsupref  46264  limsupbnd1f  46265  limsuppnfd  46281  climinf2  46286  limsuppnf  46290  climinfmpt  46294  climinf3  46295  limsupmnflem  46299  limsupmnf  46300  limsupre2  46304  limsupmnfuzlem  46305  limsupre2mpt  46309  limsupre3lem  46311  limsupre3  46312  limsupre3mpt  46313  limsupre3uzlem  46314  limsupre3uz  46315  limsupreuz  46316  limsupreuzmpt  46318  liminfval2  46347  liminfreuzlem  46381  liminfreuz  46382  xlimpnfxnegmnf  46393  cnrefiisplem  46408  xlimpnfv  46417  xlimpnf  46421  xlimpnfmpt  46423  dfxlim2  46427  icccncfext  46466  cncficcgt0  46467  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  stoweidlem5  46584  stoweidlem20  46599  stoweidlem26  46605  stoweidlem28  46607  stoweidlem29  46608  stoweidlem34  46613  wallispilem3  46646  stirlinglem13  46665  fourierdlem41  46727  fourierdlem42  46728  fourierdlem51  46736  fourierdlem54  46739  salunicl  46895  saluncl  46896  salexct  46913  salexct2  46918  salexct3  46921  salgencntex  46922  salgensscntex  46923  sge0pnffigt  46975  meadjuni  47036  omeunile  47084  ovnlerp  47141  hoidifhspval  47187  ovolval5lem2  47232  salpreimagelt  47286  pimincfltioo  47297  salpreimagtge  47304  salpreimagtlt  47309  incsmf  47321  issmfgt  47335  smfpreimagt  47341  decsmf  47346  issmfge  47349  smfpimgtxr  47359  smfpreimage  47361  smfinflem  47396  smfinf  47397  finfdm  47425  funressnfv  47642  funressnvmo  47644  funressnmo  47645  dfdfat2  47727  tz6.12-afv  47772  funressndmafv2rn  47822  tz6.12-afv2  47839  dfatcolem  47854  dfatco  47855  zplusmodne  47948  m1modne  47953  minusmod5ne  47954  submodneaddmod  47956  modmknepk  47967  iccpartigtl  48034  iccpartgt  48038  icceuelpartlem  48046  iccpartnel  48049  sprsymrelfolem2  48104  nprmmul2  48139  goldbachthlem2  48160  odz2prm2pw  48177  fmtnoprmfac1  48179  fmtnoprmfac2  48181  fmtnofac2  48183  fmtno4prmfac  48186  fmtno4prm  48189  prmdvdsfmtnof1lem1  48198  31prm  48211  nprmdvdsfacm1  48238  perfectALTVlem2  48349  nnsum3primes4  48415  nnsum3primesprm  48417  nnsum3primesgbe  48419  nnsum3primesle9  48421  nnsum4primeseven  48427  nnsum4primesevenALTV  48428  wtgoldbnnsum4prm  48429  bgoldbnnsum3prm  48431  bgoldbtbndlem4  48435  bgoldbtbnd  48436  tgblthelfgott  48442  tgoldbach  48444  assintop  48836  isassintop  48837  assintopcllaw  48839  ztprmneprm  48974  ply1mulgsumlem1  49013  ply1mulgsumlem2  49014  lco0  49054  lcoel0  49055  lincsumcl  49058  lincscmcl  49059  lcoss  49063  linindslinci  49075  lindslinindsimp1  49084  linds0  49092  el0ldep  49093  lindsrng01  49095  ldepspr  49100  islindeps2  49110  isldepslvec2  49112  zlmodzxzldep  49131  ldepsnlinc  49135  elbigo2r  49180  xpco2  49483  tposres0  49503  lubsscl  49586  glbsscl  49587  lubprlem  49588  ipolub  49614  ipoglb  49617  catprslem  49636  infsubc2  49687  nelsubc3lem  49696  cnelsubclem  50229  setrec2lem1  50319