Theorem breq1 5089

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

Assertion

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

Proof of Theorem breq1

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

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

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

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

This theorem is referenced by:  breq12  5091  breq1i  5093  breq1d  5096  nbrne2  5106  brab1  5134  pocl  5544  swopolem  5546  swopo  5547  po2ne  5552  solin  5563  sotrieq  5567  sotr2  5570  isso2i  5573  somo  5575  dffr2  5589  frc  5591  frirr  5604  fr2nr  5605  wereu2  5625  vtoclr  5691  frsn  5716  brcog  5819  brcogw  5821  brcnvg  5832  dfdmf  5849  eldmg  5851  dmun  5863  dm0rn0  5877  dfrnf  5903  dmcosseq  5931  dmcosseqOLD  5932  dfres2  6004  imasng  6047  cotrg  6072  cnvsym  6075  asymref2  6078  sotri2  6090  somin1  6094  rnco  6214  coi1  6225  predtrss  6284  frpomin  6302  dffun2  6506  dffun6f  6511  funmo  6512  fun11  6570  fveq2  6838  eliman0  6875  nfunsn  6877  dffv2  6933  fvopab5  6979  dff3  7050  f1ompt  7061  fmptco  7080  dff13  7206  foeqcnvco  7252  isorel  7278  soisores  7279  soisoi  7280  isocnv  7282  isotr  7288  isomin  7289  isoini  7290  isopolem  7297  isosolem  7299  f1oiso  7303  f1oiso2  7304  weniso  7306  eqfunresadj  7312  caovordig  7569  caovordg  7571  caovord3d  7574  caovord  7575  caovord3  7577  caofrss  7667  caoftrn  7669  fr3nr  7723  dfwe2  7725  f1oweALT  7922  frxp  8073  poxp  8075  fnse  8080  poxp2  8090  frxp2  8091  poxp3  8097  frxp3  8098  xpord3pred  8099  poseq  8105  brtpos2  8179  rntpos  8186  tpostpos  8193  frrlem12  8244  ertr  8656  ecopovsym  8763  ecopovtrn  8764  isfi  8919  en0  8962  en0ALT  8963  en1  8968  endisj  8999  xpcomco  9002  sbth  9032  2pwne  9068  disjenex  9070  ssenen  9086  findcard  9095  findcard2  9096  pssnn  9100  sbthfi  9130  nneneq  9137  php  9138  onomeneq  9145  sdom1  9157  1sdom2dom  9161  isinf  9172  fineqvlem  9173  en1eqsnbi  9183  findcard3  9190  frfi  9192  fiint  9234  mapfienlem1  9315  mapfienlem2  9316  mapfienlem3  9317  mapfien  9318  marypha1lem  9343  supmo  9362  eqsup  9366  supub  9369  suplub  9370  suppr  9382  supisolem  9384  supisoex  9385  infmin  9406  infmo  9407  fiinfg  9411  fiinf2g  9412  infpr  9415  ordtypecbv  9429  ordtypelem3  9432  ordtypelem6  9435  ordtypelem7  9436  ordtypelem9  9438  ordtypelem10  9439  hartogslem1  9454  hartogs  9456  wemaplem1  9458  wemaplem2  9459  wemapso2lem  9464  card2on  9466  card2inf  9467  elharval  9473  brwdom2  9485  wdomtr  9487  cantnfs  9584  cantnfp1lem2  9597  oemapso  9600  cantnflem1  9607  wemapwe  9615  ttrclss  9638  r111  9696  kardex  9815  karden  9816  isnumi  9867  tskwe  9871  cardid2  9874  cardonle  9878  cardne  9886  iscard2  9897  infxpenlem  9932  fodomfi2  9979  wdomfil  9980  wdomnumr  9983  alephsuc2  9999  infenaleph  10010  iunfictbso  10033  infpss  10135  cff1  10177  cfslb2n  10187  sornom  10196  fin4i  10217  isfin6  10219  isfin7  10220  isfin1-3  10305  fin1a2lem9  10327  fin1a2lem11  10329  hsmexlem4  10348  axcc2lem  10355  axcc4dom  10360  domtriomlem  10361  numthcor  10413  zorn2lem2  10416  zorn2lem3  10417  zorn2lem7  10421  zorn2g  10422  axdclem  10438  axdc  10440  brdom7disj  10450  brdom6disj  10451  uniimadom  10463  ondomon  10482  alephval2  10492  alephreg  10502  pwcfsdom  10503  elgch  10542  gchi  10544  fpwwe2lem11  10561  fpwwe2lem12  10562  winainflem  10613  winalim2  10616  tsken  10674  0tsk  10675  inar1  10695  tskord  10700  tskuni  10703  grudomon  10737  pinq  10847  nqereu  10849  enqeq  10854  ltbtwnnq  10898  ltrnq  10899  prcdnq  10913  prnmax  10915  genpnmax  10927  nqpr  10934  1idpr  10949  reclem2pr  10968  reclem3pr  10969  reclem4pr  10970  recexpr  10971  supexpr  10974  ltsosr  11014  1ne0sr  11016  ltasr  11020  supsrlem  11031  axpre-lttri  11085  axpre-lttrn  11086  axpre-ltadd  11087  axpre-sup  11089  lelttr  11233  dedekind  11306  dedekindle  11307  ltordlem  11672  lt0ne0d  11712  fimaxre3  12099  fiminre2  12101  lbreu  12103  lble  12105  sup2  12109  infm3  12112  suprleub  12119  supaddc  12120  supadd  12121  supmul1  12122  supmullem1  12123  supmul  12125  nnne0  12208  nnsub  12218  nominpos  12411  nnunb  12430  arch  12431  nn0sub  12484  nn0n0n1ge2b  12503  nn0lt10b  12588  zextle  12599  peano5uzti  12616  fzind  12624  btwnz  12629  uzval  12787  uzwo  12858  nnwof  12861  ublbneg  12880  lbzbi  12883  zsupss  12884  uzsupss  12887  uzwo3  12890  zmax  12892  rebtwnz  12894  rpnnen1lem3  12926  xrltnsym  13085  xrlttri  13087  xrlttr  13088  xrlelttr  13104  nltpnft  13113  xrmaxlt  13130  xrmaxle  13132  qbtwnre  13148  qbtwnxr  13149  xltnegi  13165  xnn0lenn0nn0  13194  xsubge0  13210  xlesubadd  13212  xmullem2  13214  xlemul1a  13237  xrinfmexpnf  13255  xrsupsslem  13256  xrinfmsslem  13257  xrub  13261  supxrunb1  13268  supxrunb2  13269  reltre  13290  rpltrp  13291  reltxrnmnf  13292  ixxval  13303  elixx1  13304  elioo2  13336  iccid  13340  icc0  13343  fzval  13460  elfz1  13463  elfznelfzo  13725  elfznelfzob  13726  flval  13750  fllelt  13753  flflp1  13763  flval2  13770  flval3  13771  flbi  13772  dfceil2  13795  ceilval2  13796  fleqceilz  13810  modid2  13854  addmodlteq  13905  fsequb2  13935  ssnn0fi  13944  seqf1olem2  14001  sqlecan  14168  faclbnd4lem1  14252  hashsnle1  14376  pr2pwpr  14438  hash3tpde  14452  rtrclreclem3  15019  relexpindlem  15022  sgnval  15047  01sqrexlem6  15206  01sqrex  15208  abslt  15274  absle  15275  rexanre  15306  rexico  15313  limsupgle  15436  limsupgre  15440  limsupbnd2  15442  rlim2lt  15456  rlim3  15457  ello12r  15476  ello1d  15482  elo12r  15487  rlimconst  15503  climshft  15535  rlimcn3  15549  o1rlimmul  15578  lo1le  15611  climsup  15629  caucvgrlem  15632  isumless  15807  divrcnv  15814  cvgrat  15845  rpnnen2lem10  16187  ruclem1  16195  ruclem2  16196  ruclem11  16204  ruclem12  16205  sqrt2irr  16213  absdvdsb  16240  dvdsle  16276  dvdsabseq  16279  dvdsdivcl  16282  dvdsext  16287  divalglem8  16366  divalglem9  16367  divalglem10  16368  divalgmod  16372  ndvdssub  16375  sadcaddlem  16423  gcdcllem1  16465  gcdcllem2  16466  gcdcllem3  16467  dfgcd2  16512  gcdzeq  16518  dvdssq  16533  nn0seqcvgd  16536  algcvgblem  16543  lcmval  16558  lcmdvds  16574  lcmgcdeq  16578  lcmfpr  16593  lcmf  16599  lcmftp  16602  lcmfunsnlem1  16603  lcmfunsnlem2lem1  16604  lcmfunsnlem2lem2  16605  lcmfdvdsb  16609  coprmgcdb  16615  coprmdvds1  16618  1nprm  16645  1idssfct  16646  isprm2lem  16647  isprm2  16648  dvdsprime  16653  nprm  16654  3prm  16660  dvdsprm  16670  exprmfct  16671  isprm5  16674  maxprmfct  16676  coprm  16678  prmdvdsncoprmbd  16694  ncoprmlnprm  16695  eulerthlem2  16749  phisum  16758  odzval  16759  pythagtriplem4  16787  pc2dvds  16847  pcprmpw2  16850  pcprmpw  16851  dvdsprmpweqle  16854  oddprmdvds  16871  prmpwdvds  16872  pockthg  16874  unbenlem  16876  prmreclem4  16887  prmreclem5  16888  prmreclem6  16889  1arith  16895  vdwlem6  16954  vdwlem11  16959  vdwlem13  16961  ramtlecl  16968  ramub  16981  rami  16983  ramubcl  16986  0ram  16988  ram0  16990  prmdvdsprmop  17011  prmolefac  17014  prmodvdslcmf  17015  prmgaplem2  17018  prmgaplcmlem1  17019  prmgaplcmlem2  17020  prmgaplem3  17021  prmgaplem4  17022  prmgaplem5  17023  prmgaplem6  17024  prmgapprmolem  17029  prmlem0  17073  prmlem1a  17074  imasaddfnlem  17489  imasvscafn  17498  imasleval  17502  prslem  18260  drsdir  18265  drsdirfi  18268  isdrs2  18269  posi  18280  posasymb  18282  pospropd  18288  pltval3  18300  plelttr  18305  pospo  18306  lubprop  18319  luble  18320  lublecllem  18321  glbprop  18332  joinval2lem  18341  joinlem  18344  meetlem  18358  meetle  18361  poslubmo  18372  posglbmo  18373  poslubd  18374  tleile  18382  latnlej  18419  isglbd  18472  lubub  18474  lubun  18478  clatleglb  18481  tsrlin  18548  letsr  18556  dirge  18566  pmtrval  19423  pmtrrn  19429  pmtrfrn  19430  pmtrrn2  19432  pmtrsn  19491  mndodcongi  19515  odeq  19522  odmulgeq  19529  gexnnod  19560  sylow1lem1  19570  pgpssslw  19586  sylow2a  19591  efgredeu  19724  efgred2  19725  gexex  19825  frgpnabllem2  19846  cyggenod  19856  dprdval  19977  dprdw  19984  dprdwd  19985  ablfacrplem  20039  ablfac1c  20045  ablfac1eu  20047  ablfaclem3  20061  omndadd  20100  abvtrivd  20806  zringlpir  21463  prmirredlem  21468  znleval  21550  frlmelbas  21752  ellspd  21798  islindf4  21834  psrbagconcl  21923  psrbagleadd1  21924  gsumbagdiaglem  21926  rhmpsrlem2  21936  psrlidm  21956  psrridm  21957  psrass1  21958  psrcom  21962  mplelbas  21985  mplmonmul  22030  ltbwe  22038  mhpmulcl  22131  psdmul  22148  coe1fsupp  22194  coe1ae0  22196  coe1mul2  22250  coe1tmmul  22258  pmatcoe1fsupp  22682  chfacffsupp  22837  chfacfscmulfsupp  22840  chfacfscmulgsum  22841  chfacfpmmulfsupp  22844  chfacfpmmulgsum  22845  ordtbas2  23172  ordtopn2  23176  ordtrest2lem  23184  pnfnei  23201  ordtt1  23360  ordthauslem  23364  2ndci  23429  2ndcsb  23430  2ndcredom  23431  2ndc1stc  23432  1stcrest  23434  2ndcctbss  23436  2ndcdisj  23437  2ndcsep  23440  lly1stc  23477  tx1stc  23631  ordthmeolem  23782  ufildom1  23907  xmetrtri2  24337  prdsxmetlem  24349  ssblex  24409  prdsbl  24472  comet  24494  stdbdxmet  24496  stdbdmopn  24499  met1stc  24502  dscmet  24553  metdstri  24833  metdscn  24838  xrhmeo  24929  bndth  24941  evth  24942  lebnumlem3  24946  pcovalg  24995  pco1  24998  pcocn  25000  pcopt  25005  pcopt2  25006  pcoass  25007  nmoleub3  25102  bcthlem5  25311  rrxfsupp  25385  minveclem4c  25408  minveclem2  25409  minveclem3b  25411  minveclem4  25415  minveclem6  25417  pmltpclem1  25431  pmltpc  25433  ovollb2lem  25471  ovolctb  25473  ovolunlem1  25480  ovoliunlem1  25485  ovoliunlem2  25486  ovoliun2  25489  ovolshftlem1  25492  ovolscalem1  25496  ovolicc1  25499  ovolicc2lem3  25502  voliunlem2  25534  voliunlem3  25535  ioombl1lem4  25544  uniioovol  25562  uniioombllem2  25566  uniioombllem3  25568  uniioombllem6  25571  volsup2  25588  ismbfd  25622  mbfsup  25647  mbflimsup  25649  itg1climres  25697  mbfi1fseqlem4  25701  itg2lr  25713  itg2leub  25717  itg2seq  25725  itg2monolem1  25733  itg2monolem3  25735  itg2mono  25736  itg2i1fseq2  25739  itg2gt0  25743  itg2cnlem1  25744  itg2cnlem2  25745  itg2cn  25746  iblss  25788  itgless  25800  ibladdlem  25803  iblabsr  25813  iblmulc2  25814  itgabs  25818  bddiblnc  25825  ditgeq1  25831  dvferm2lem  25969  rolle  25973  dvlip2  25978  c1liplem1  25979  c1lip1  25980  dvfsumlem2  26010  dvfsumlem4  26012  mdegleb  26045  degltlem1  26053  plyco0  26173  plyeq0lem  26191  coeeq2  26223  dgrle  26224  dgradd2  26249  plydiveu  26281  aareccl  26309  aalioulem2  26316  aaliou3lem7  26332  psercnlem1  26409  pilem2  26436  pilem3  26437  logltb  26583  divlogrlim  26618  logcnlem3  26627  cxpaddlelem  26734  rlimcnp  26948  cxplim  26955  cxploglim  26961  scvxcvx  26969  ftalem1  27056  ftalem2  27057  isppw2  27098  vmappw  27099  sgmnncl  27130  sqff1o  27165  fsumdvdsdiaglem  27166  dvdsppwf1o  27169  dvdsflsumcom  27171  musum  27174  muinv  27176  mpodvdsmulf1o  27177  dvdsmulf1o  27179  vmalelog  27188  vmasum  27199  logfac2  27200  perfectlem2  27213  bcmono  27260  bpos1lem  27265  bposlem9  27275  lgsmod  27306  lgsne0  27318  gausslemma2dlem4  27352  2sqlem6  27406  2sqlem8  27409  2sqlem10  27411  2sqreulem1  27429  2sqreunnlem1  27432  chtppilim  27458  rpvmasumlem  27470  dchrisumlema  27471  dchrisumlem2  27473  dchrvmasumlem1  27478  dchrvmasumiflem1  27484  dchrisum0flblem1  27491  dchrisum0flblem2  27492  dchrisum0  27503  rplogsum  27510  logsqvma  27525  pntpbnd1  27569  pntpbnd2  27570  pntibndlem3  27575  pntlemj  27586  pntlemi  27587  pntlem3  27592  pnt3  27595  ostth3  27621  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  29900  crctcshwlkn0lem3  29901  crctcsh  29913  wlkswwlksf1o  29968  clwlkclwwlklem2fv1  30086  clwlkclwwlkf  30099  0clwlkv  30222  eupth2  30330  numclwwlk5  30479  nmoubi  30864  minvecolem2  30967  minvecolem3  30968  minvecolem4c  30971  minvecolem4  30972  minvecolem5  30973  minvecolem6  30974  htthlem  31009  chlimi  31326  chcompl  31334  hsn0elch  31340  cmbr3  31700  cmcm  31706  cmcm3  31707  lecm  31709  nmopub  32000  nmfnleub  32017  nmopun  32106  nmcexi  32118  cnlnadjlem7  32165  pjnmopi  32240  stle0i  32331  stlesi  32333  stm1i  32335  csmdsymi  32426  cvmd  32428  atcveq0  32440  atcv1  32472  atord  32480  atcvat2  32481  chirred  32487  mdsym  32504  mddmdin0i  32523  cdj1i  32525  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  33182  fzto1st  33185  psgnfzto1st  33187  trsp2cyc  33205  xrnarchi  33266  archirng  33270  archiexdiv  33272  archiabl  33280  isarchiofld  33281  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  linds2eq  33462  elrspunidl  33509  elrspunsn  33510  isrprm  33598  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  extvfvvcl  33700  extvfvcl  33701  mplmulmvr  33704  evlextv  33707  mplvrpmlem  33708  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  psrmonmul  33715  psrmonprod  33717  esplyfval0  33729  esplylem  33731  esplyfv1  33734  esplyfval3  33737  esplyfvaln  33739  esplyind  33740  ply1degltdimlem  33788  lbsdiflsp0  33792  fedgmullem1  33795  fedgmullem2  33796  fedgmul  33797  fldextrspunlsplem  33839  fldextrspunlsp  33840  smatrcl  33962  smatlem  33963  madjusmdetlem2  33994  madjusmdet  33997  cmpcref  34016  ldlfcntref  34020  dispcmp  34025  zarcmplem  34047  ordtrest2NEWlem  34088  ordtconnlem1  34090  xrge0iifiso  34101  rge0scvg  34115  gsumesum  34225  esumfsup  34236  esumpinfval  34239  esumpcvgval  34244  esumcvg  34252  sigaclcu  34283  sigaclci  34298  unelsiga  34300  unelldsys  34324  sigapildsys  34328  ldgenpisyslem1  34329  fiunelros  34340  measvun  34375  voliune  34395  volfiniune  34396  oms0  34463  omssubaddlem  34465  omssubadd  34466  carsgsigalem  34481  carsgclctunlem2  34485  carsgclctun  34487  pmeasmono  34490  pmeasadd  34491  orvcval2  34625  dstfrvel  34640  ballotlemfc0  34659  ballotlemfcc  34660  ballotlemsv  34676  ballotlemsf1o  34680  breprexp  34799  tgoldbachgt  34829  bnj23  34883  bnj1185  34957  bnj1152  35162  bnj1418  35204  fnrelpredd  35256  loop1cycl  35341  umgr2cycl  35345  acycgrcycl  35351  dfdm5  35977  dfrn5  35978  wzel  36026  wsuclem  36027  brpprod  36087  brsset  36091  brbigcup  36100  dffix2  36107  elfuns  36117  brimageg  36129  brdomaing  36137  brrangeg  36138  brimg  36139  brapply  36140  lemsuccf  36143  funpartlem  36146  brrestrict  36153  dfrecs2  36154  dfrdg4  36155  brofs  36209  btwncomim  36217  btwnintr  36223  btwnexch3  36224  btwnexch2  36227  brifs  36247  brcolinear2  36262  colineardim1  36265  brfs  36283  btwnconn1  36305  segcon2  36309  seglerflx  36316  seglemin  36317  btwnsegle  36321  colinbtwnle  36322  broutsideof2  36326  fvray  36345  lineunray  36351  lineelsb2  36352  linerflx1  36353  trer  36520  elicc3  36521  finminlem  36522  nn0prpwlem  36526  nn0prpw  36527  fnessref  36561  refssfne  36562  weiunlem  36667  weiunfrlem  36668  weiunfr  36671  weiunse  36672  unblimceq0lem  36788  unblimceq0  36789  unbdqndv2  36793  knoppndvlem21  36814  taupilemrplb  37656  dfgcd3  37660  icorempo  37689  icoreval  37691  iooelexlt  37700  relowlssretop  37701  domalom  37742  ctbssinf  37744  pibt2  37755  phpreu  37947  fin2solem  37949  fin2so  37950  ltflcei  37951  ptrecube  37963  poimirlem1  37964  poimirlem2  37965  poimirlem5  37968  poimirlem6  37969  poimirlem7  37970  poimirlem9  37972  poimirlem12  37975  poimirlem22  37985  poimirlem23  37986  poimirlem24  37987  poimirlem26  37989  poimirlem27  37990  poimirlem32  37995  heicant  37998  mblfinlem1  38000  mblfinlem2  38001  itg2addnclem  38014  itg2addnclem3  38016  itg2addnc  38017  itg2gt0cn  38018  ibladdnclem  38019  iblmulc2nc  38028  itgabsnc  38032  ftc1anclem5  38040  ftc1anclem7  38042  ftc1anclem8  38043  ftc1anc  38044  indexdom  38077  filbcmb  38083  fdc  38088  prdsbnd  38136  heiborlem3  38156  rrnequiv  38178  rngoueqz  38283  eqbrtr  38581  elrnressn  38623  inxprnres  38641  presucmap  38838  eqvreltr  39034  prtlem10  39333  lsatcveq0  39500  lsatcv1  39516  oposlem  39650  opnlen0  39656  lub0N  39657  glb0N  39661  omllaw  39711  cmtbr4N  39723  cvrval  39737  cvrnbtwn  39739  cvrnbtwn2  39743  cvrnbtwn3  39744  cvrcon3b  39745  cvrnbtwn4  39747  atcvreq0  39782  atnle  39785  atlatmstc  39787  cvlexch1  39796  glbconN  39845  hlsuprexch  39849  exatleN  39872  cvratlem  39889  atcvrj0  39896  atcvrj2b  39900  atlelt  39906  cvrat4  39911  3dim1lem5  39934  3dim2  39936  3dim3  39937  ps-2  39946  llni  39976  llnn0  39984  llnle  39986  lplni  40000  lplni2  40005  lplnle  40008  lplnn0N  40015  llncvrlpln  40026  2llnjN  40035  lvoli  40043  lvoli3  40045  lvoli2  40049  lvoln0N  40059  4at  40081  lplncvrlvol  40084  2lplnj  40088  dalemcea  40128  dalem3  40132  psubspi  40215  linepsubN  40220  elpmap  40226  pmapsub  40236  lnatexN  40247  cdlema1N  40259  cdlemb  40262  elpadd  40267  paddvaln0N  40269  paddasslem5  40292  llnexchb2lem  40336  llnexch2N  40338  islhp  40464  lhpat3  40514  4atexlemex2  40539  4atex  40544  4atex2-0aOLDN  40546  4atex2-0cOLDN  40548  lautle  40552  lautcvr  40560  lauteq  40563  ldilval  40581  ltrnu  40589  trlval2  40631  trlne  40653  cdleme0ex1N  40691  cdleme0nex  40758  cdleme18d  40763  cdlemednuN  40768  cdleme25b  40822  cdleme25cv  40826  cdleme27b  40836  cdleme29b  40843  cdleme31sn  40848  cdleme31fv  40858  cdleme31fv2  40861  cdlemefrs29bpre0  40864  cdlemefr29bpre0N  40874  cdlemefr29clN  40875  cdlemefr32fvaN  40877  cdlemefr32fva1  40878  cdlemefs29pre00N  40880  cdlemefs32sn1aw  40882  cdlemefs29bpre0N  40884  cdlemefs29bpre1N  40885  cdlemefs29cpre1N  40886  cdlemefs29clN  40887  cdlemefs32fvaN  40890  cdlemefs32fva1  40891  cdleme41sn3a  40901  cdleme32fva  40905  cdleme32e  40913  cdleme35f  40922  cdleme40v  40937  cdleme42b  40946  trlord  41037  cdlemg1cex  41056  diaval  41500  diaeldm  41504  diaelrnN  41513  cdlemm10N  41586  dibglbN  41634  dicval  41644  dicfnN  41651  dicvalrelN  41653  dihval  41700  dihlsscpre  41702  dihglblem3N  41763  dihmeetlem2N  41767  djhcvat42  41883  lcmineqlem4  42493  aks4d1p4  42540  aks4d1p5  42541  aks4d1p7  42544  aks4d1p8d2  42546  aks4d1p8  42548  hashnexinjle  42590  sticksstones1  42607  sticksstones2  42608  sticksstones10  42616  sticksstones12a  42618  aks6d1c7lem4  42644  aks6d1c7  42645  grpods  42655  unitscyglem2  42657  unitscyglem3  42658  unitscyglem4  42659  qsalrel  42702  supinf  42703  dvdsexpnn0  42788  redvmptabs  42814  sn-nnne0  42927  sn-sup2  42958  fimgmcyclem  43000  flt4lem2  43102  flt4lem7  43114  lzenom  43224  fphpdo  43271  irrapxlem4  43279  pellexlem6  43288  infmrgelbi  43332  pellfundre  43335  pellfundlb  43338  monotoddzz  43397  zindbi  43400  jm2.27  43462  rmydioph  43468  rpnnen3lem  43485  fnwe2lem2  43505  aomclem8  43515  hbtlem5  43582  hbt  43584  sdomne0  43866  sdomne0d  43867  ensucne0  43982  sucomisnotcard  43997  en2pr  44000  pr2cv  44001  refimssco  44060  rfovfvfvd  44456  rfovcnvf1od  44457  fsovrfovd  44462  nzss  44770  relprel  45404  permaxinf2lem  45465  wessf1ornlem  45641  axccdom  45677  dmrelrnrel  45681  axccd  45684  rnmptlb  45698  rnmptbdd  45700  rnmptbd2  45704  rnmptbdlem  45710  rnmptbd  45711  dstregt0  45741  suplesup  45795  supxrunb3  45854  supxrleubrnmpt  45860  rexabslelem  45872  rexabsle  45873  suprleubrnmpt  45876  infrnmptle  45877  infxrunb3rnmpt  45882  infxrpnf  45900  supminfxr  45918  infrpgernmpt  45919  xrpnf  45939  limsupre  46095  limsupref  46139  limsupbnd1f  46140  limsuppnfd  46156  climinf2  46161  limsuppnf  46165  climinfmpt  46169  climinf3  46170  limsupmnflem  46174  limsupmnf  46175  limsupre2  46179  limsupmnfuzlem  46180  limsupre2mpt  46184  limsupre3lem  46186  limsupre3  46187  limsupre3mpt  46188  limsupre3uzlem  46189  limsupre3uz  46190  limsupreuz  46191  limsupreuzmpt  46193  liminfval2  46222  liminfreuzlem  46256  liminfreuz  46257  xlimpnfxnegmnf  46268  cnrefiisplem  46283  xlimpnfv  46292  xlimpnf  46296  xlimpnfmpt  46298  dfxlim2  46302  icccncfext  46341  cncficcgt0  46342  ioodvbdlimc1lem2  46386  ioodvbdlimc2lem  46388  stoweidlem5  46459  stoweidlem20  46474  stoweidlem26  46480  stoweidlem28  46482  stoweidlem29  46483  stoweidlem34  46488  wallispilem3  46521  stirlinglem13  46540  fourierdlem41  46602  fourierdlem42  46603  fourierdlem51  46611  fourierdlem54  46614  salunicl  46770  saluncl  46771  salexct  46788  salexct2  46793  salexct3  46796  salgencntex  46797  salgensscntex  46798  sge0pnffigt  46850  meadjuni  46911  omeunile  46959  ovnlerp  47016  hoidifhspval  47062  ovolval5lem2  47107  salpreimagelt  47161  pimincfltioo  47172  salpreimagtge  47179  salpreimagtlt  47184  incsmf  47196  issmfgt  47210  smfpreimagt  47216  decsmf  47221  issmfge  47224  smfpimgtxr  47234  smfpreimage  47236  smfinflem  47271  smfinf  47272  finfdm  47300  funressnfv  47511  funressnvmo  47513  funressnmo  47514  dfdfat2  47596  tz6.12-afv  47641  funressndmafv2rn  47691  tz6.12-afv2  47708  dfatcolem  47723  dfatco  47724  zplusmodne  47817  m1modne  47822  minusmod5ne  47823  submodneaddmod  47825  modmknepk  47836  iccpartigtl  47903  iccpartgt  47907  icceuelpartlem  47915  iccpartnel  47918  sprsymrelfolem2  47973  nprmmul2  48008  goldbachthlem2  48029  odz2prm2pw  48046  fmtnoprmfac1  48048  fmtnoprmfac2  48050  fmtnofac2  48052  fmtno4prmfac  48055  fmtno4prm  48058  prmdvdsfmtnof1lem1  48067  31prm  48080  nprmdvdsfacm1  48107  perfectALTVlem2  48218  nnsum3primes4  48284  nnsum3primesprm  48286  nnsum3primesgbe  48288  nnsum3primesle9  48290  nnsum4primeseven  48296  nnsum4primesevenALTV  48297  wtgoldbnnsum4prm  48298  bgoldbnnsum3prm  48300  bgoldbtbndlem4  48304  bgoldbtbnd  48305  tgblthelfgott  48311  tgoldbach  48313  assintop  48705  isassintop  48706  assintopcllaw  48708  ztprmneprm  48843  ply1mulgsumlem1  48882  ply1mulgsumlem2  48883  lco0  48923  lcoel0  48924  lincsumcl  48927  lincscmcl  48928  lcoss  48932  linindslinci  48944  lindslinindsimp1  48953  linds0  48961  el0ldep  48962  lindsrng01  48964  ldepspr  48969  islindeps2  48979  isldepslvec2  48981  zlmodzxzldep  49000  ldepsnlinc  49004  elbigo2r  49049  xpco2  49352  tposres0  49372  lubsscl  49455  glbsscl  49456  lubprlem  49457  ipolub  49483  ipoglb  49486  catprslem  49505  infsubc2  49556  nelsubc3lem  49565  cnelsubclem  50098  setrec2lem1  50188