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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ⟨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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  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  5844  eldmg  5846  dmun  5858  dm0rn0  5872  dfrnf  5898  dmcosseq  5926  dmcosseqOLD  5927  dfres2  5999  imasng  6042  cotrg  6067  cnvsym  6070  asymref2  6073  sotri2  6085  somin1  6089  rnco  6206  coi1  6217  predtrss  6276  frpomin  6294  dffun2  6498  dffun6f  6503  funmo  6504  fun11  6562  fveq2  6830  eliman0  6867  nfunsn  6869  dffv2  6925  fvopab5  6972  dff3  7044  f1ompt  7055  fmptco  7074  dff13  7201  foeqcnvco  7247  isorel  7273  soisores  7274  soisoi  7275  isocnv  7277  isotr  7283  isomin  7284  isoini  7285  isopolem  7292  isosolem  7294  f1oiso  7298  f1oiso2  7299  weniso  7301  eqfunresadj  7307  caovordig  7564  caovordg  7566  caovord3d  7569  caovord  7570  caovord3  7572  caofrss  7662  caoftrn  7664  fr3nr  7718  dfwe2  7720  f1oweALT  7916  frxp  8068  poxp  8070  fnse  8075  poxp2  8085  frxp2  8086  poxp3  8092  frxp3  8093  xpord3pred  8094  poseq  8100  brtpos2  8174  rntpos  8181  tpostpos  8188  frrlem12  8240  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  9582  cantnfp1lem2  9595  oemapso  9598  cantnflem1  9605  wemapwe  9613  ttrclss  9636  r111  9694  kardex  9813  karden  9814  isnumi  9865  tskwe  9869  cardid2  9872  cardonle  9876  cardne  9884  iscard2  9895  infxpenlem  9930  fodomfi2  9977  wdomfil  9978  wdomnumr  9981  alephsuc2  9997  infenaleph  10008  iunfictbso  10031  infpss  10133  cff1  10176  cfslb2n  10186  sornom  10195  fin4i  10216  isfin6  10218  isfin7  10219  isfin1-3  10304  fin1a2lem9  10326  fin1a2lem11  10328  hsmexlem4  10347  axcc2lem  10354  axcc4dom  10359  domtriomlem  10360  numthcor  10412  zorn2lem2  10415  zorn2lem3  10416  zorn2lem7  10420  zorn2g  10421  axdclem  10437  axdc  10439  brdom7disj  10449  brdom6disj  10450  uniimadom  10462  ondomon  10481  alephval2  10491  alephreg  10501  pwcfsdom  10502  elgch  10541  gchi  10543  fpwwe2lem11  10560  fpwwe2lem12  10561  winainflem  10612  winalim2  10615  tsken  10673  0tsk  10674  inar1  10694  tskord  10699  tskuni  10702  grudomon  10736  pinq  10846  nqereu  10848  enqeq  10853  ltbtwnnq  10897  ltrnq  10898  prcdnq  10912  prnmax  10914  genpnmax  10926  nqpr  10933  1idpr  10948  reclem2pr  10967  reclem3pr  10968  reclem4pr  10969  recexpr  10970  supexpr  10973  ltsosr  11013  1ne0sr  11015  ltasr  11019  supsrlem  11030  axpre-lttri  11084  axpre-lttrn  11085  axpre-ltadd  11086  axpre-sup  11088  lelttr  11232  dedekind  11305  dedekindle  11306  ltordlem  11671  lt0ne0d  11711  fimaxre3  12097  fiminre2  12099  lbreu  12101  lble  12103  sup2  12107  infm3  12110  suprleub  12117  supaddc  12118  supadd  12119  supmul1  12120  supmullem1  12121  supmul  12123  nnne0  12206  nnsub  12216  nominpos  12409  nnunb  12428  arch  12429  nn0sub  12482  nn0n0n1ge2b  12501  nn0lt10b  12586  zextle  12597  peano5uzti  12614  fzind  12622  btwnz  12627  uzval  12785  uzwo  12856  nnwof  12859  ublbneg  12878  lbzbi  12881  zsupss  12882  uzsupss  12885  uzwo3  12888  zmax  12890  rebtwnz  12892  rpnnen1lem3  12924  xrltnsym  13083  xrlttri  13085  xrlttr  13086  xrlelttr  13102  nltpnft  13111  xrmaxlt  13128  xrmaxle  13130  qbtwnre  13146  qbtwnxr  13147  xltnegi  13163  xnn0lenn0nn0  13192  xsubge0  13208  xlesubadd  13210  xmullem2  13212  xlemul1a  13235  xrinfmexpnf  13253  xrsupsslem  13254  xrinfmsslem  13255  xrub  13259  supxrunb1  13266  supxrunb2  13267  reltre  13288  rpltrp  13289  reltxrnmnf  13290  ixxval  13301  elixx1  13302  elioo2  13334  iccid  13338  icc0  13341  fzval  13458  elfz1  13461  elfznelfzo  13723  elfznelfzob  13724  flval  13748  fllelt  13751  flflp1  13761  flval2  13768  flval3  13769  flbi  13770  dfceil2  13793  ceilval2  13794  fleqceilz  13808  modid2  13852  addmodlteq  13903  fsequb2  13933  ssnn0fi  13942  seqf1olem2  13999  sqlecan  14166  faclbnd4lem1  14250  hashsnle1  14374  pr2pwpr  14436  hash3tpde  14450  rtrclreclem3  15017  relexpindlem  15020  sgnval  15045  01sqrexlem6  15204  01sqrex  15206  abslt  15272  absle  15273  rexanre  15304  rexico  15311  limsupgle  15434  limsupgre  15438  limsupbnd2  15440  rlim2lt  15454  rlim3  15455  ello12r  15474  ello1d  15480  elo12r  15485  rlimconst  15501  climshft  15533  rlimcn3  15547  o1rlimmul  15576  lo1le  15609  climsup  15627  caucvgrlem  15630  isumless  15805  divrcnv  15812  cvgrat  15843  rpnnen2lem10  16185  ruclem1  16193  ruclem2  16194  ruclem11  16202  ruclem12  16203  sqrt2irr  16211  absdvdsb  16238  dvdsle  16274  dvdsabseq  16277  dvdsdivcl  16280  dvdsext  16285  divalglem8  16364  divalglem9  16365  divalglem10  16366  divalgmod  16370  ndvdssub  16373  sadcaddlem  16421  gcdcllem1  16463  gcdcllem2  16464  gcdcllem3  16465  dfgcd2  16510  gcdzeq  16516  dvdssq  16531  nn0seqcvgd  16534  algcvgblem  16541  lcmval  16556  lcmdvds  16572  lcmgcdeq  16576  lcmfpr  16591  lcmf  16597  lcmftp  16600  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem2lem2  16603  lcmfdvdsb  16607  coprmgcdb  16613  coprmdvds1  16616  1nprm  16643  1idssfct  16644  isprm2lem  16645  isprm2  16646  dvdsprime  16651  nprm  16652  3prm  16658  dvdsprm  16668  exprmfct  16669  isprm5  16672  maxprmfct  16674  coprm  16676  prmdvdsncoprmbd  16692  ncoprmlnprm  16693  eulerthlem2  16747  phisum  16756  odzval  16757  pythagtriplem4  16785  pc2dvds  16845  pcprmpw2  16848  pcprmpw  16849  dvdsprmpweqle  16852  oddprmdvds  16869  prmpwdvds  16870  pockthg  16872  unbenlem  16874  prmreclem4  16885  prmreclem5  16886  prmreclem6  16887  1arith  16893  vdwlem6  16952  vdwlem11  16957  vdwlem13  16959  ramtlecl  16966  ramub  16979  rami  16981  ramubcl  16984  0ram  16986  ram0  16988  prmdvdsprmop  17009  prmolefac  17012  prmodvdslcmf  17013  prmgaplem2  17016  prmgaplcmlem1  17017  prmgaplcmlem2  17018  prmgaplem3  17019  prmgaplem4  17020  prmgaplem5  17021  prmgaplem6  17022  prmgapprmolem  17027  prmlem0  17071  prmlem1a  17072  imasaddfnlem  17487  imasvscafn  17496  imasleval  17500  prslem  18258  drsdir  18263  drsdirfi  18266  isdrs2  18267  posi  18278  posasymb  18280  pospropd  18286  pltval3  18298  plelttr  18303  pospo  18304  lubprop  18317  luble  18318  lublecllem  18319  glbprop  18330  joinval2lem  18339  joinlem  18342  meetlem  18356  meetle  18359  poslubmo  18370  posglbmo  18371  poslubd  18372  tleile  18380  latnlej  18417  isglbd  18470  lubub  18472  lubun  18476  clatleglb  18479  tsrlin  18546  letsr  18554  dirge  18564  pmtrval  19420  pmtrrn  19426  pmtrfrn  19427  pmtrrn2  19429  pmtrsn  19488  mndodcongi  19512  odeq  19519  odmulgeq  19526  gexnnod  19557  sylow1lem1  19567  pgpssslw  19583  sylow2a  19588  efgredeu  19721  efgred2  19722  gexex  19822  frgpnabllem2  19843  cyggenod  19853  dprdval  19974  dprdw  19981  dprdwd  19982  ablfacrplem  20036  ablfac1c  20042  ablfac1eu  20044  ablfaclem3  20058  omndadd  20097  abvtrivd  20807  zringlpir  21445  prmirredlem  21450  znleval  21532  frlmelbas  21734  ellspd  21780  islindf4  21816  psrbagconcl  21905  psrbagleadd1  21906  gsumbagdiaglem  21909  rhmpsrlem2  21919  psrlidm  21939  psrridm  21940  psrass1  21941  psrcom  21945  mplelbas  21968  mplmonmul  22015  ltbwe  22023  mhpmulcl  22140  psdmul  22157  coe1fsupp  22202  coe1ae0  22204  coe1mul2  22258  coe1tmmul  22266  pmatcoe1fsupp  22687  chfacffsupp  22842  chfacfscmulfsupp  22845  chfacfscmulgsum  22846  chfacfpmmulfsupp  22849  chfacfpmmulgsum  22850  ordtbas2  23177  ordtopn2  23181  ordtrest2lem  23189  pnfnei  23206  ordtt1  23365  ordthauslem  23369  2ndci  23434  2ndcsb  23435  2ndcredom  23436  2ndc1stc  23437  1stcrest  23439  2ndcctbss  23441  2ndcdisj  23442  2ndcsep  23445  lly1stc  23482  tx1stc  23636  ordthmeolem  23787  ufildom1  23912  xmetrtri2  24342  prdsxmetlem  24354  ssblex  24414  prdsbl  24477  comet  24499  stdbdxmet  24501  stdbdmopn  24504  met1stc  24507  dscmet  24558  metdstri  24838  metdscn  24843  xrhmeo  24934  bndth  24946  evth  24947  lebnumlem3  24951  pcovalg  25000  pco1  25003  pcocn  25005  pcopt  25010  pcopt2  25011  pcoass  25012  nmoleub3  25107  bcthlem5  25316  rrxfsupp  25390  minveclem4c  25413  minveclem2  25414  minveclem3b  25416  minveclem4  25420  minveclem6  25422  pmltpclem1  25436  pmltpc  25438  ovollb2lem  25476  ovolctb  25478  ovolunlem1  25485  ovoliunlem1  25490  ovoliunlem2  25491  ovoliun2  25494  ovolshftlem1  25497  ovolscalem1  25501  ovolicc1  25504  ovolicc2lem3  25507  voliunlem2  25539  voliunlem3  25540  ioombl1lem4  25549  uniioovol  25567  uniioombllem2  25571  uniioombllem3  25573  uniioombllem6  25576  volsup2  25593  ismbfd  25627  mbfsup  25652  mbflimsup  25654  itg1climres  25702  mbfi1fseqlem4  25706  itg2lr  25718  itg2leub  25722  itg2seq  25730  itg2monolem1  25738  itg2monolem3  25740  itg2mono  25741  itg2i1fseq2  25744  itg2gt0  25748  itg2cnlem1  25749  itg2cnlem2  25750  itg2cn  25751  iblss  25793  itgless  25805  ibladdlem  25808  iblabsr  25818  iblmulc2  25819  itgabs  25823  bddiblnc  25830  ditgeq1  25836  dvferm2lem  25974  rolle  25978  dvlip2  25983  c1liplem1  25984  c1lip1  25985  dvfsumlem2  26015  dvfsumlem4  26017  mdegleb  26050  degltlem1  26058  plyco0  26178  plyeq0lem  26196  coeeq2  26228  dgrle  26229  dgradd2  26254  plydiveu  26285  aareccl  26313  aalioulem2  26320  aaliou3lem7  26336  psercnlem1  26411  pilem2  26438  pilem3  26439  logltb  26585  divlogrlim  26620  logcnlem3  26629  cxpaddlelem  26736  rlimcnp  26950  cxplim  26956  cxploglim  26962  scvxcvx  26970  ftalem1  27057  ftalem2  27058  isppw2  27099  vmappw  27100  sgmnncl  27131  sqff1o  27166  fsumdvdsdiaglem  27167  dvdsppwf1o  27170  dvdsflsumcom  27172  musum  27175  muinv  27177  mpodvdsmulf1o  27178  dvdsmulf1o  27180  vmalelog  27189  vmasum  27200  logfac2  27201  perfectlem2  27214  bcmono  27261  bpos1lem  27266  bposlem9  27276  lgsmod  27307  lgsne0  27319  gausslemma2dlem4  27353  2sqlem6  27407  2sqlem8  27410  2sqlem10  27412  2sqreulem1  27430  2sqreunnlem1  27433  chtppilim  27459  rpvmasumlem  27471  dchrisumlema  27472  dchrisumlem2  27474  dchrvmasumlem1  27479  dchrvmasumiflem1  27485  dchrisum0flblem1  27492  dchrisum0flblem2  27493  dchrisum0  27504  rplogsum  27511  logsqvma  27526  pntpbnd1  27570  pntpbnd2  27571  pntibndlem3  27576  pntlemj  27587  pntlemi  27588  pntlem3  27593  pnt3  27596  ostth3  27622  nodense  27676  noresle  27681  nosupprefixmo  27684  noinfprefixmo  27685  nosupcbv  27686  nosupdm  27688  nosupbnd1lem1  27692  nosupbnd1lem4  27695  nosupbnd1  27698  nosupbnd2lem1  27699  nosupbnd2  27700  noinfcbv  27701  noinfdm  27703  noinffv  27705  noinfres  27706  noinfbnd1lem3  27709  noinfbnd1lem4  27710  noinfbnd1lem5  27711  noinfbnd1  27713  noetalem2  27726  nocvxminlem  27766  sltssnb  27781  sltssepc  27783  conway  27791  cutsval  27792  etaslts  27805  lesrec  27811  eqcuts3  27816  bday1  27826  cuteq1  27829  madeval2  27845  rightval  27862  elleft  27863  sltsright  27873  made0  27875  madecut  27895  left1s  27907  madebdaylemlrcut  27911  ltslpss  27920  cofslts  27930  coinitslts  27931  cofcutr  27936  cofcutrtime  27939  cofss  27942  coiniss  27943  cutmax  27946  cutmin  27947  cutminmax  27948  addsproplem1  27981  addsprop  27988  leadds1  28001  addsuniflem  28013  negsproplem1  28040  negsprop  28047  negsid  28053  negsunif  28067  mulsproplemcbv  28127  mulsproplem1  28128  mulsproplem9  28136  mulsprop  28142  sltmuls1  28159  sltmuls2  28160  mulsuniflem  28161  precsexlem11  28229  abslts  28261  oncutlt  28276  oniso  28283  bdayons  28288  addonbday  28291  n0fincut  28367  onsfi  28368  n0subs  28375  bdayn0p1  28381  eucliddivs  28388  zcuts  28419  twocut  28435  halfcut  28470  addhalfcut  28471  bdaypw2n0bndlem  28475  bdayfinbndcbv  28478  bdayfinbndlem1  28479  bdayfinbndlem2  28480  z12bdaylem1  28482  elreno  28503  elreno2  28507  tgjustc1  28563  tgjustc2  28564  iscgrglt  28602  tgcgr4  28619  hlcgreu  28706  lmif  28873  islmib  28875  trgcopyeu  28894  iscgrad  28899  inaghl  28933  axlowdim2  29049  axlowdim  29050  axcontlem2  29054  axcontlem3  29055  axcontlem4  29056  axcontlem7  29059  axcontlem9  29061  axcontlem10  29062  axcontlem11  29063  axcontlem12  29064  ebtwntg  29071  umgrupgr  29192  nbusgrvtxm1  29468  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  32751  fnpreimac  32764  isoun  32796  fcobijfs  32815  fcobijfs2  32816  lt2addrd  32844  xlt2addrd  32853  xrge0infss  32854  infxrge0glb  32859  xrofsup  32861  fz1nnct  32895  sgnmulsgn  32936  toslublem  33053  tosglblem  33055  ismntd  33065  mgccole1  33071  mgccole2  33072  mgcmnt1  33073  mgcmnt2  33074  dfmgc2lem  33076  dfmgc2  33077  psgnfzto1stlem  33183  fzto1st  33186  psgnfzto1st  33188  trsp2cyc  33206  xrnarchi  33267  archirng  33271  archiexdiv  33273  archiabl  33281  isarchiofld  33282  elrgspnlem1  33325  elrgspnlem2  33326  elrgspnlem3  33327  elrgspnlem4  33328  elrgspn  33329  elrgspnsubrunlem1  33330  elrgspnsubrunlem2  33331  elrgspnsubrun  33332  linds2eq  33466  elrspunidl  33513  elrspunsn  33514  isrprm  33610  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  0mplrim  33708  selvply1rhmlema  33712  selvply1rhmlemb  33713  selvply1rhmlem1  33714  selvply1rhmlem2  33715  selvply1rhmlem4  33717  selvply1rhm0  33720  extvfvvcl  33729  extvfvcl  33730  mplmulmvr  33733  evlextv  33736  mplvrpmlem  33737  mplvrpmfgalem  33738  mplvrpmga  33739  mplvrpmmhm  33740  mplvrpmrhm  33741  psrmonmul  33744  psrmonprod  33746  esplyfval0  33758  esplylem  33760  esplyfv1  33763  esplyfval3  33766  esplyfvaln  33768  esplyind  33769  ply1degltdimlem  33816  lbsdiflsp0  33820  fedgmullem1  33823  fedgmullem2  33824  fedgmul  33825  fldextrspunlsplem  33867  fldextrspunlsp  33868  smatrcl  33990  smatlem  33991  madjusmdetlem2  34022  madjusmdet  34025  cmpcref  34044  ldlfcntref  34048  dispcmp  34053  zarcmplem  34075  ordtrest2NEWlem  34116  ordtconnlem1  34118  xrge0iifiso  34129  rge0scvg  34143  gsumesum  34253  esumfsup  34264  esumpinfval  34267  esumpcvgval  34272  esumcvg  34280  sigaclcu  34311  sigaclci  34326  unelsiga  34328  unelldsys  34352  sigapildsys  34356  ldgenpisyslem1  34357  fiunelros  34368  measvun  34403  voliune  34423  volfiniune  34424  oms0  34491  omssubaddlem  34493  omssubadd  34494  carsgsigalem  34509  carsgclctunlem2  34513  carsgclctun  34515  pmeasmono  34518  pmeasadd  34519  orvcval2  34653  dstfrvel  34668  ballotlemfc0  34687  ballotlemfcc  34688  ballotlemsv  34704  ballotlemsf1o  34708  breprexp  34827  tgoldbachgt  34857  bnj23  34914  bnj1185  34988  bnj1152  35193  bnj1418  35235  fnrelpredd  35285  loop1cycl  35378  umgr2cycl  35382  acycgrcycl  35388  dfdm5  36014  dfrn5  36015  wzel  36063  wsuclem  36064  brpprod  36124  brsset  36128  brbigcup  36137  dffix2  36144  elfuns  36154  brimageg  36166  brdomaing  36174  brrangeg  36175  brimg  36176  brapply  36177  lemsuccf  36180  funpartlem  36183  brrestrict  36190  dfrecs2  36191  dfrdg4  36192  brofs  36246  btwncomim  36254  btwnintr  36260  btwnexch3  36261  btwnexch2  36264  brifs  36284  brcolinear2  36299  colineardim1  36302  brfs  36320  btwnconn1  36342  segcon2  36346  seglerflx  36353  seglemin  36354  btwnsegle  36358  colinbtwnle  36359  broutsideof2  36363  fvray  36382  lineunray  36388  lineelsb2  36389  linerflx1  36390  trer  36557  elicc3  36558  finminlem  36559  nn0prpwlem  36563  nn0prpw  36564  fnessref  36598  refssfne  36599  weiunlem  36704  weiunfrlem  36705  weiunfr  36708  weiunse  36709  unblimceq0lem  36825  unblimceq0  36826  unbdqndv2  36830  knoppndvlem21  36851  taupilemrplb  37693  dfgcd3  37697  icorempo  37726  icoreval  37728  iooelexlt  37737  relowlssretop  37738  domalom  37779  ctbssinf  37781  pibt2  37792  phpreu  37984  fin2solem  37986  fin2so  37987  ltflcei  37988  ptrecube  38000  poimirlem1  38001  poimirlem2  38002  poimirlem5  38005  poimirlem6  38006  poimirlem7  38007  poimirlem9  38009  poimirlem12  38012  poimirlem22  38022  poimirlem23  38023  poimirlem24  38024  poimirlem26  38026  poimirlem27  38027  poimirlem32  38032  heicant  38035  mblfinlem1  38037  mblfinlem2  38038  itg2addnclem  38051  itg2addnclem3  38053  itg2addnc  38054  itg2gt0cn  38055  ibladdnclem  38056  iblmulc2nc  38065  itgabsnc  38069  ftc1anclem5  38077  ftc1anclem7  38079  ftc1anclem8  38080  ftc1anc  38081  indexdom  38114  filbcmb  38120  fdc  38125  prdsbnd  38173  heiborlem3  38193  rrnequiv  38215  rngoueqz  38320  eqbrtr  38618  elrnressn  38660  inxprnres  38678  presucmap  38875  eqvreltr  39071  prtlem10  39370  lsatcveq0  39537  lsatcv1  39553  oposlem  39687  opnlen0  39693  lub0N  39694  glb0N  39698  omllaw  39748  cmtbr4N  39760  cvrval  39774  cvrnbtwn  39776  cvrnbtwn2  39780  cvrnbtwn3  39781  cvrcon3b  39782  cvrnbtwn4  39784  atcvreq0  39819  atnle  39822  atlatmstc  39824  cvlexch1  39833  glbconN  39882  hlsuprexch  39886  exatleN  39909  cvratlem  39926  atcvrj0  39933  atcvrj2b  39937  atlelt  39943  cvrat4  39948  3dim1lem5  39971  3dim2  39973  3dim3  39974  ps-2  39983  llni  40013  llnn0  40021  llnle  40023  lplni  40037  lplni2  40042  lplnle  40045  lplnn0N  40052  llncvrlpln  40063  2llnjN  40072  lvoli  40080  lvoli3  40082  lvoli2  40086  lvoln0N  40096  4at  40118  lplncvrlvol  40121  2lplnj  40125  dalemcea  40165  dalem3  40169  psubspi  40252  linepsubN  40257  elpmap  40263  pmapsub  40273  lnatexN  40284  cdlema1N  40296  cdlemb  40299  elpadd  40304  paddvaln0N  40306  paddasslem5  40329  llnexchb2lem  40373  llnexch2N  40375  islhp  40501  lhpat3  40551  4atexlemex2  40576  4atex  40581  4atex2-0aOLDN  40583  4atex2-0cOLDN  40585  lautle  40589  lautcvr  40597  lauteq  40600  ldilval  40618  ltrnu  40626  trlval2  40668  trlne  40690  cdleme0ex1N  40728  cdleme0nex  40795  cdleme18d  40800  cdlemednuN  40805  cdleme25b  40859  cdleme25cv  40863  cdleme27b  40873  cdleme29b  40880  cdleme31sn  40885  cdleme31fv  40895  cdleme31fv2  40898  cdlemefrs29bpre0  40901  cdlemefr29bpre0N  40911  cdlemefr29clN  40912  cdlemefr32fvaN  40914  cdlemefr32fva1  40915  cdlemefs29pre00N  40917  cdlemefs32sn1aw  40919  cdlemefs29bpre0N  40921  cdlemefs29bpre1N  40922  cdlemefs29cpre1N  40923  cdlemefs29clN  40924  cdlemefs32fvaN  40927  cdlemefs32fva1  40928  cdleme41sn3a  40938  cdleme32fva  40942  cdleme32e  40950  cdleme35f  40959  cdleme40v  40974  cdleme42b  40983  trlord  41074  cdlemg1cex  41093  diaval  41537  diaeldm  41541  diaelrnN  41550  cdlemm10N  41623  dibglbN  41671  dicval  41681  dicfnN  41688  dicvalrelN  41690  dihval  41737  dihlsscpre  41739  dihglblem3N  41800  dihmeetlem2N  41804  djhcvat42  41920  lcmineqlem4  42530  aks4d1p4  42577  aks4d1p5  42578  aks4d1p7  42581  aks4d1p8d2  42583  aks4d1p8  42585  hashnexinjle  42627  sticksstones1  42644  sticksstones2  42645  sticksstones10  42653  sticksstones12a  42655  aks6d1c7lem4  42681  aks6d1c7  42682  grpods  42692  unitscyglem2  42694  unitscyglem3  42695  unitscyglem4  42696  qsalrel  42738  supinf  42739  dvdsexpnn0  42824  redvmptabs  42850  sn-nnne0  42963  sn-sup2  42994  fimgmcyclem  43032  flt4lem2  43110  flt4lem7  43122  lzenom  43232  fphpdo  43275  irrapxlem4  43283  pellexlem6  43292  infmrgelbi  43336  pellfundre  43339  pellfundlb  43342  monotoddzz  43401  zindbi  43404  jm2.27  43466  rmydioph  43472  rpnnen3lem  43489  fnwe2lem2  43509  aomclem8  43519  hbtlem5  43586  hbt  43588  sdomne0  43870  sdomne0d  43871  ensucne0  43986  sucomisnotcard  44001  en2pr  44004  pr2cv  44005  refimssco  44064  rfovfvfvd  44460  rfovcnvf1od  44461  fsovrfovd  44466  nzss  44774  relprel  45408  permaxinf2lem  45469  wessf1ornlem  45644  axccdom  45679  dmrelrnrel  45683  axccd  45685  rnmptlb  45699  rnmptbdd  45701  rnmptbd2  45705  rnmptbdlem  45711  rnmptbd  45712  dstregt0  45742  suplesup  45796  supxrunb3  45855  supxrleubrnmpt  45861  rexabslelem  45873  rexabsle  45874  suprleubrnmpt  45877  infrnmptle  45878  infxrunb3rnmpt  45883  infxrpnf  45901  supminfxr  45919  infrpgernmpt  45920  xrpnf  45940  limsupre  46096  limsupref  46140  limsupbnd1f  46141  limsuppnfd  46157  climinf2  46162  limsuppnf  46166  climinfmpt  46170  climinf3  46171  limsupmnflem  46175  limsupmnf  46176  limsupre2  46180  limsupmnfuzlem  46181  limsupre2mpt  46185  limsupre3lem  46187  limsupre3  46188  limsupre3mpt  46189  limsupre3uzlem  46190  limsupre3uz  46191  limsupreuz  46192  limsupreuzmpt  46194  liminfval2  46223  liminfreuzlem  46257  liminfreuz  46258  xlimpnfxnegmnf  46269  cnrefiisplem  46284  xlimpnfv  46293  xlimpnf  46297  xlimpnfmpt  46299  dfxlim2  46303  icccncfext  46342  cncficcgt0  46343  ioodvbdlimc1lem2  46387  ioodvbdlimc2lem  46389  stoweidlem5  46460  stoweidlem20  46475  stoweidlem26  46481  stoweidlem28  46483  stoweidlem29  46484  stoweidlem34  46489  wallispilem3  46522  stirlinglem13  46541  fourierdlem41  46603  fourierdlem42  46604  fourierdlem51  46612  fourierdlem54  46615  salunicl  46771  saluncl  46772  salexct  46789  salexct2  46794  salexct3  46797  salgencntex  46798  salgensscntex  46799  sge0pnffigt  46851  meadjuni  46912  omeunile  46960  ovnlerp  47017  hoidifhspval  47063  ovolval5lem2  47108  salpreimagelt  47162  pimincfltioo  47173  salpreimagtge  47180  salpreimagtlt  47185  incsmf  47197  issmfgt  47211  smfpreimagt  47217  decsmf  47222  issmfge  47225  smfpimgtxr  47235  smfpreimage  47237  smfinflem  47272  smfinf  47273  finfdm  47301  funressnfv  47518  funressnvmo  47520  funressnmo  47521  dfdfat2  47603  tz6.12-afv  47648  funressndmafv2rn  47698  tz6.12-afv2  47715  dfatcolem  47730  dfatco  47731  zplusmodne  47824  m1modne  47829  minusmod5ne  47830  submodneaddmod  47832  modmknepk  47843  iccpartigtl  47910  iccpartgt  47914  icceuelpartlem  47922  iccpartnel  47925  sprsymrelfolem2  47980  nprmmul2  48015  goldbachthlem2  48036  odz2prm2pw  48053  fmtnoprmfac1  48055  fmtnoprmfac2  48057  fmtnofac2  48059  fmtno4prmfac  48062  fmtno4prm  48065  prmdvdsfmtnof1lem1  48074  31prm  48087  nprmdvdsfacm1  48114  perfectALTVlem2  48225  nnsum3primes4  48291  nnsum3primesprm  48293  nnsum3primesgbe  48295  nnsum3primesle9  48297  nnsum4primeseven  48303  nnsum4primesevenALTV  48304  wtgoldbnnsum4prm  48305  bgoldbnnsum3prm  48307  bgoldbtbndlem4  48311  bgoldbtbnd  48312  tgblthelfgott  48318  tgoldbach  48320  assintop  48712  isassintop  48713  assintopcllaw  48715  ztprmneprm  48850  ply1mulgsumlem1  48889  ply1mulgsumlem2  48890  lco0  48930  lcoel0  48931  lincsumcl  48934  lincscmcl  48935  lcoss  48939  linindslinci  48951  lindslinindsimp1  48960  linds0  48968  el0ldep  48969  lindsrng01  48971  ldepspr  48976  islindeps2  48986  isldepslvec2  48988  zlmodzxzldep  49007  ldepsnlinc  49011  elbigo2r  49056  xpco2  49359  tposres0  49379  lubsscl  49462  glbsscl  49463  lubprlem  49464  ipolub  49490  ipoglb  49493  catprslem  49512  infsubc2  49563  nelsubc3lem  49572  cnelsubclem  50105  setrec2lem1  50195