Theorem breq1 5103

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breq12  5105  breq1i  5107  breq1d  5110  nbrne2  5120  brab1  5148  pocl  5550  swopolem  5552  swopo  5553  po2ne  5558  solin  5569  sotrieq  5573  sotr2  5576  isso2i  5579  somo  5581  dffr2  5595  frc  5597  frirr  5610  fr2nr  5611  wereu2  5631  vtoclr  5697  frsn  5722  brcog  5825  brcogw  5827  brcnvg  5838  dfdmf  5855  eldmg  5857  dmun  5869  dm0rn0  5883  dfrnf  5909  dmcosseq  5937  dmcosseqOLD  5938  dfres2  6010  imasng  6053  cotrg  6078  cnvsym  6081  asymref2  6084  sotri2  6096  somin1  6100  rnco  6220  coi1  6231  predtrss  6290  frpomin  6308  dffun2  6512  dffun6f  6517  funmo  6518  fun11  6576  fveq2  6844  eliman0  6881  nfunsn  6883  dffv2  6939  fvopab5  6985  dff3  7056  f1ompt  7067  fmptco  7086  dff13  7212  foeqcnvco  7258  isorel  7284  soisores  7285  soisoi  7286  isocnv  7288  isotr  7294  isomin  7295  isoini  7296  isopolem  7303  isosolem  7305  f1oiso  7309  f1oiso2  7310  weniso  7312  eqfunresadj  7318  caovordig  7575  caovordg  7577  caovord3d  7580  caovord  7581  caovord3  7583  caofrss  7673  caoftrn  7675  fr3nr  7729  dfwe2  7731  f1oweALT  7928  frxp  8080  poxp  8082  fnse  8087  poxp2  8097  frxp2  8098  poxp3  8104  frxp3  8105  xpord3pred  8106  poseq  8112  brtpos2  8186  rntpos  8193  tpostpos  8200  frrlem12  8251  ertr  8663  ecopovsym  8770  ecopovtrn  8771  isfi  8926  en0  8969  en0ALT  8970  en1  8975  endisj  9006  xpcomco  9009  sbth  9039  2pwne  9075  disjenex  9077  ssenen  9093  findcard  9102  findcard2  9103  pssnn  9107  sbthfi  9137  nneneq  9144  php  9145  onomeneq  9152  sdom1  9164  1sdom2dom  9168  isinf  9179  fineqvlem  9180  en1eqsnbi  9190  findcard3  9197  frfi  9199  fiint  9241  mapfienlem1  9322  mapfienlem2  9323  mapfienlem3  9324  mapfien  9325  marypha1lem  9350  supmo  9369  eqsup  9373  supub  9376  suplub  9377  suppr  9389  supisolem  9391  supisoex  9392  infmin  9413  infmo  9414  fiinfg  9418  fiinf2g  9419  infpr  9422  ordtypecbv  9436  ordtypelem3  9439  ordtypelem6  9442  ordtypelem7  9443  ordtypelem9  9445  ordtypelem10  9446  hartogslem1  9461  hartogs  9463  wemaplem1  9465  wemaplem2  9466  wemapso2lem  9471  card2on  9473  card2inf  9474  elharval  9480  brwdom2  9492  wdomtr  9494  cantnfs  9589  cantnfp1lem2  9602  oemapso  9605  cantnflem1  9612  wemapwe  9620  ttrclss  9643  r111  9701  kardex  9820  karden  9821  isnumi  9872  tskwe  9876  cardid2  9879  cardonle  9883  cardne  9891  iscard2  9902  infxpenlem  9937  fodomfi2  9984  wdomfil  9985  wdomnumr  9988  alephsuc2  10004  infenaleph  10015  iunfictbso  10038  infpss  10140  cff1  10182  cfslb2n  10192  sornom  10201  fin4i  10222  isfin6  10224  isfin7  10225  isfin1-3  10310  fin1a2lem9  10332  fin1a2lem11  10334  hsmexlem4  10353  axcc2lem  10360  axcc4dom  10365  domtriomlem  10366  numthcor  10418  zorn2lem2  10421  zorn2lem3  10422  zorn2lem7  10426  zorn2g  10427  axdclem  10443  axdc  10445  brdom7disj  10455  brdom6disj  10456  uniimadom  10468  ondomon  10487  alephval2  10497  alephreg  10507  pwcfsdom  10508  elgch  10547  gchi  10549  fpwwe2lem11  10566  fpwwe2lem12  10567  winainflem  10618  winalim2  10621  tsken  10679  0tsk  10680  inar1  10700  tskord  10705  tskuni  10708  grudomon  10742  pinq  10852  nqereu  10854  enqeq  10859  ltbtwnnq  10903  ltrnq  10904  prcdnq  10918  prnmax  10920  genpnmax  10932  nqpr  10939  1idpr  10954  reclem2pr  10973  reclem3pr  10974  reclem4pr  10975  recexpr  10976  supexpr  10979  ltsosr  11019  1ne0sr  11021  ltasr  11025  supsrlem  11036  axpre-lttri  11090  axpre-lttrn  11091  axpre-ltadd  11092  axpre-sup  11094  lelttr  11237  dedekind  11310  dedekindle  11311  ltordlem  11676  lt0ne0d  11716  fimaxre3  12102  fiminre2  12104  lbreu  12106  lble  12108  sup2  12112  infm3  12115  suprleub  12122  supaddc  12123  supadd  12124  supmul1  12125  supmullem1  12126  supmul  12128  nnne0  12193  nnsub  12203  nominpos  12392  nnunb  12411  arch  12412  nn0sub  12465  nn0n0n1ge2b  12484  nn0lt10b  12568  zextle  12579  peano5uzti  12596  fzind  12604  btwnz  12609  uzval  12767  uzwo  12838  nnwof  12841  ublbneg  12860  lbzbi  12863  zsupss  12864  uzsupss  12867  uzwo3  12870  zmax  12872  rebtwnz  12874  rpnnen1lem3  12906  xrltnsym  13065  xrlttri  13067  xrlttr  13068  xrlelttr  13084  nltpnft  13093  xrmaxlt  13110  xrmaxle  13112  qbtwnre  13128  qbtwnxr  13129  xltnegi  13145  xnn0lenn0nn0  13174  xsubge0  13190  xlesubadd  13192  xmullem2  13194  xlemul1a  13217  xrinfmexpnf  13235  xrsupsslem  13236  xrinfmsslem  13237  xrub  13241  supxrunb1  13248  supxrunb2  13249  reltre  13270  rpltrp  13271  reltxrnmnf  13272  ixxval  13283  elixx1  13284  elioo2  13316  iccid  13320  icc0  13323  fzval  13439  elfz1  13442  elfznelfzo  13703  elfznelfzob  13704  flval  13728  fllelt  13731  flflp1  13741  flval2  13748  flval3  13749  flbi  13750  dfceil2  13773  ceilval2  13774  fleqceilz  13788  modid2  13832  addmodlteq  13883  fsequb2  13913  ssnn0fi  13922  seqf1olem2  13979  sqlecan  14146  faclbnd4lem1  14230  hashsnle1  14354  pr2pwpr  14416  hash3tpde  14430  rtrclreclem3  14997  relexpindlem  15000  sgnval  15025  01sqrexlem6  15184  01sqrex  15186  abslt  15252  absle  15253  rexanre  15284  rexico  15291  limsupgle  15414  limsupgre  15418  limsupbnd2  15420  rlim2lt  15434  rlim3  15435  ello12r  15454  ello1d  15460  elo12r  15465  rlimconst  15481  climshft  15513  rlimcn3  15527  o1rlimmul  15556  lo1le  15589  climsup  15607  caucvgrlem  15610  isumless  15782  divrcnv  15789  cvgrat  15820  rpnnen2lem10  16162  ruclem1  16170  ruclem2  16171  ruclem11  16179  ruclem12  16180  sqrt2irr  16188  absdvdsb  16215  dvdsle  16251  dvdsabseq  16254  dvdsdivcl  16257  dvdsext  16262  divalglem8  16341  divalglem9  16342  divalglem10  16343  divalgmod  16347  ndvdssub  16350  sadcaddlem  16398  gcdcllem1  16440  gcdcllem2  16441  gcdcllem3  16442  dfgcd2  16487  gcdzeq  16493  dvdssq  16508  nn0seqcvgd  16511  algcvgblem  16518  lcmval  16533  lcmdvds  16549  lcmgcdeq  16553  lcmfpr  16568  lcmf  16574  lcmftp  16577  lcmfunsnlem1  16578  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  lcmfdvdsb  16584  coprmgcdb  16590  coprmdvds1  16593  1nprm  16620  1idssfct  16621  isprm2lem  16622  isprm2  16623  dvdsprime  16628  nprm  16629  3prm  16635  dvdsprm  16644  exprmfct  16645  isprm5  16648  maxprmfct  16650  coprm  16652  prmdvdsncoprmbd  16668  ncoprmlnprm  16669  eulerthlem2  16723  phisum  16732  odzval  16733  pythagtriplem4  16761  pc2dvds  16821  pcprmpw2  16824  pcprmpw  16825  dvdsprmpweqle  16828  oddprmdvds  16845  prmpwdvds  16846  pockthg  16848  unbenlem  16850  prmreclem4  16861  prmreclem5  16862  prmreclem6  16863  1arith  16869  vdwlem6  16928  vdwlem11  16933  vdwlem13  16935  ramtlecl  16942  ramub  16955  rami  16957  ramubcl  16960  0ram  16962  ram0  16964  prmdvdsprmop  16985  prmolefac  16988  prmodvdslcmf  16989  prmgaplem2  16992  prmgaplcmlem1  16993  prmgaplcmlem2  16994  prmgaplem3  16995  prmgaplem4  16996  prmgaplem5  16997  prmgaplem6  16998  prmgapprmolem  17003  prmlem0  17047  prmlem1a  17048  imasaddfnlem  17463  imasvscafn  17472  imasleval  17476  prslem  18234  drsdir  18239  drsdirfi  18242  isdrs2  18243  posi  18254  posasymb  18256  pospropd  18262  pltval3  18274  plelttr  18279  pospo  18280  lubprop  18293  luble  18294  lublecllem  18295  glbprop  18306  joinval2lem  18315  joinlem  18318  meetlem  18332  meetle  18335  poslubmo  18346  posglbmo  18347  poslubd  18348  tleile  18356  latnlej  18393  isglbd  18446  lubub  18448  lubun  18452  clatleglb  18455  tsrlin  18522  letsr  18530  dirge  18540  pmtrval  19397  pmtrrn  19403  pmtrfrn  19404  pmtrrn2  19406  pmtrsn  19465  mndodcongi  19489  odeq  19496  odmulgeq  19503  gexnnod  19534  sylow1lem1  19544  pgpssslw  19560  sylow2a  19565  efgredeu  19698  efgred2  19699  gexex  19799  frgpnabllem2  19820  cyggenod  19830  dprdval  19951  dprdw  19958  dprdwd  19959  ablfacrplem  20013  ablfac1c  20019  ablfac1eu  20021  ablfaclem3  20035  omndadd  20074  abvtrivd  20782  zringlpir  21439  prmirredlem  21444  znleval  21526  frlmelbas  21728  ellspd  21774  islindf4  21810  psrbagconcl  21900  psrbagleadd1  21901  gsumbagdiaglem  21903  rhmpsrlem2  21914  psrlidm  21934  psrridm  21935  psrass1  21936  psrcom  21940  mplelbas  21963  mplmonmul  22008  ltbwe  22016  mhpmulcl  22109  psdmul  22126  coe1fsupp  22172  coe1ae0  22174  coe1mul2  22228  coe1tmmul  22236  pmatcoe1fsupp  22662  chfacffsupp  22817  chfacfscmulfsupp  22820  chfacfscmulgsum  22821  chfacfpmmulfsupp  22824  chfacfpmmulgsum  22825  ordtbas2  23152  ordtopn2  23156  ordtrest2lem  23164  pnfnei  23181  ordtt1  23340  ordthauslem  23344  2ndci  23409  2ndcsb  23410  2ndcredom  23411  2ndc1stc  23412  1stcrest  23414  2ndcctbss  23416  2ndcdisj  23417  2ndcsep  23420  lly1stc  23457  tx1stc  23611  ordthmeolem  23762  ufildom1  23887  xmetrtri2  24317  prdsxmetlem  24329  ssblex  24389  prdsbl  24452  comet  24474  stdbdxmet  24476  stdbdmopn  24479  met1stc  24482  dscmet  24533  metdstri  24813  metdscn  24818  xrhmeo  24917  bndth  24930  evth  24931  lebnumlem3  24935  pcovalg  24985  pco1  24988  pcocn  24990  pcopt  24995  pcopt2  24996  pcoass  24997  nmoleub3  25092  bcthlem5  25301  rrxfsupp  25375  minveclem4c  25398  minveclem2  25399  minveclem3b  25401  minveclem4  25405  minveclem6  25407  pmltpclem1  25422  pmltpc  25424  ovollb2lem  25462  ovolctb  25464  ovolunlem1  25471  ovoliunlem1  25476  ovoliunlem2  25477  ovoliun2  25480  ovolshftlem1  25483  ovolscalem1  25487  ovolicc1  25490  ovolicc2lem3  25493  voliunlem2  25525  voliunlem3  25526  ioombl1lem4  25535  uniioovol  25553  uniioombllem2  25557  uniioombllem3  25559  uniioombllem6  25562  volsup2  25579  ismbfd  25613  mbfsup  25638  mbflimsup  25640  itg1climres  25688  mbfi1fseqlem4  25692  itg2lr  25704  itg2leub  25708  itg2seq  25716  itg2monolem1  25724  itg2monolem3  25726  itg2mono  25727  itg2i1fseq2  25730  itg2gt0  25734  itg2cnlem1  25735  itg2cnlem2  25736  itg2cn  25737  iblss  25779  itgless  25791  ibladdlem  25794  iblabsr  25804  iblmulc2  25805  itgabs  25809  bddiblnc  25816  ditgeq1  25822  dvferm2lem  25963  rolle  25967  dvlip2  25973  c1liplem1  25974  c1lip1  25975  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem4  26009  mdegleb  26042  degltlem1  26050  plyco0  26170  plyeq0lem  26188  coeeq2  26220  dgrle  26221  dgradd2  26247  plydiveu  26279  aareccl  26307  aalioulem2  26314  aaliou3lem7  26330  psercnlem1  26408  pilem2  26435  pilem3  26436  logltb  26582  divlogrlim  26617  logcnlem3  26626  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  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  27677  noresle  27682  nosupprefixmo  27685  noinfprefixmo  27686  nosupcbv  27687  nosupdm  27689  nosupbnd1lem1  27693  nosupbnd1lem4  27696  nosupbnd1  27699  nosupbnd2lem1  27700  nosupbnd2  27701  noinfcbv  27702  noinfdm  27704  noinffv  27706  noinfres  27707  noinfbnd1lem3  27710  noinfbnd1lem4  27711  noinfbnd1lem5  27712  noinfbnd1  27714  noetalem2  27727  nocvxminlem  27767  sltssnb  27782  sltssepc  27784  conway  27792  cutsval  27793  etaslts  27806  lesrec  27812  eqcuts3  27817  bday1  27827  cuteq1  27830  madeval2  27846  rightval  27863  elleft  27864  sltsright  27874  made0  27876  madecut  27896  left1s  27908  madebdaylemlrcut  27912  ltslpss  27921  cofslts  27931  coinitslts  27932  cofcutr  27937  cofcutrtime  27940  cofss  27943  coiniss  27944  cutmax  27947  cutmin  27948  cutminmax  27949  addsproplem1  27982  addsprop  27989  leadds1  28002  addsuniflem  28014  negsproplem1  28041  negsprop  28048  negsid  28054  negsunif  28068  mulsproplemcbv  28128  mulsproplem1  28129  mulsproplem9  28137  mulsprop  28143  sltmuls1  28160  sltmuls2  28161  mulsuniflem  28162  precsexlem11  28230  abslts  28262  oncutlt  28277  oniso  28284  bdayons  28289  addonbday  28292  n0fincut  28368  onsfi  28369  n0subs  28376  bdayn0p1  28382  eucliddivs  28389  zcuts  28420  twocut  28436  halfcut  28471  addhalfcut  28472  bdaypw2n0bndlem  28476  bdayfinbndcbv  28479  bdayfinbndlem1  28480  bdayfinbndlem2  28481  z12bdaylem1  28483  elreno  28504  elreno2  28508  tgjustc1  28565  tgjustc2  28566  iscgrglt  28604  tgcgr4  28621  hlcgreu  28708  lmif  28875  islmib  28877  trgcopyeu  28896  iscgrad  28901  inaghl  28935  axlowdim2  29051  axlowdim  29052  axcontlem2  29056  axcontlem3  29057  axcontlem4  29058  axcontlem7  29061  axcontlem9  29063  axcontlem10  29064  axcontlem11  29065  axcontlem12  29066  ebtwntg  29073  umgrupgr  29194  nbusgrvtxm1  29470  crctcshwlkn0lem2  29902  crctcshwlkn0lem3  29903  crctcsh  29915  wlkswwlksf1o  29970  clwlkclwwlklem2fv1  30088  clwlkclwwlkf  30101  0clwlkv  30224  eupth2  30332  numclwwlk5  30481  nmoubi  30866  minvecolem2  30969  minvecolem3  30970  minvecolem4c  30973  minvecolem4  30974  minvecolem5  30975  minvecolem6  30976  htthlem  31011  chlimi  31328  chcompl  31336  hsn0elch  31342  cmbr3  31702  cmcm  31708  cmcm3  31709  lecm  31711  nmopub  32002  nmfnleub  32019  nmopun  32108  nmcexi  32120  cnlnadjlem7  32167  pjnmopi  32242  stle0i  32333  stlesi  32335  stm1i  32337  csmdsymi  32428  cvmd  32430  atcveq0  32442  atcv1  32474  atord  32482  atcvat2  32483  chirred  32489  mdsym  32506  mddmdin0i  32525  cdj1i  32527  fmptcof2  32753  fnpreimac  32766  isoun  32798  fcobijfs  32817  fcobijfs2  32818  lt2addrd  32847  xlt2addrd  32856  xrge0infss  32857  infxrge0glb  32862  xrofsup  32864  fz1nnct  32898  sgnmulsgn  32940  toslublem  33071  tosglblem  33073  ismntd  33083  mgccole1  33089  mgccole2  33090  mgcmnt1  33091  mgcmnt2  33092  dfmgc2lem  33094  dfmgc2  33095  psgnfzto1stlem  33200  fzto1st  33203  psgnfzto1st  33205  trsp2cyc  33223  xrnarchi  33284  archirng  33288  archiexdiv  33290  archiabl  33298  isarchiofld  33299  elrgspnlem1  33342  elrgspnlem2  33343  elrgspnlem3  33344  elrgspnlem4  33345  elrgspn  33346  elrgspnsubrunlem1  33347  elrgspnsubrunlem2  33348  elrgspnsubrun  33349  linds2eq  33480  elrspunidl  33527  elrspunsn  33528  isrprm  33616  evl1deg1  33675  evl1deg2  33676  evl1deg3  33677  extvfvvcl  33718  extvfvcl  33719  mplmulmvr  33722  evlextv  33725  mplvrpmlem  33726  mplvrpmfgalem  33727  mplvrpmga  33728  mplvrpmmhm  33729  mplvrpmrhm  33730  psrmonmul  33733  psrmonprod  33735  esplyfval0  33747  esplylem  33749  esplyfv1  33752  esplyfval3  33755  esplyfvaln  33757  esplyind  33758  ply1degltdimlem  33806  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  fldextrspunlsplem  33857  fldextrspunlsp  33858  smatrcl  33980  smatlem  33981  madjusmdetlem2  34012  madjusmdet  34015  cmpcref  34034  ldlfcntref  34038  dispcmp  34043  zarcmplem  34065  ordtrest2NEWlem  34106  ordtconnlem1  34108  xrge0iifiso  34119  rge0scvg  34133  gsumesum  34243  esumfsup  34254  esumpinfval  34257  esumpcvgval  34262  esumcvg  34270  sigaclcu  34301  sigaclci  34316  unelsiga  34318  unelldsys  34342  sigapildsys  34346  ldgenpisyslem1  34347  fiunelros  34358  measvun  34393  voliune  34413  volfiniune  34414  oms0  34481  omssubaddlem  34483  omssubadd  34484  carsgsigalem  34499  carsgclctunlem2  34503  carsgclctun  34505  pmeasmono  34508  pmeasadd  34509  orvcval2  34643  dstfrvel  34658  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemsv  34694  ballotlemsf1o  34698  breprexp  34817  tgoldbachgt  34847  bnj23  34901  bnj1185  34975  bnj1152  35180  bnj1418  35222  fnrelpredd  35274  loop1cycl  35359  umgr2cycl  35363  acycgrcycl  35369  dfdm5  35995  dfrn5  35996  wzel  36044  wsuclem  36045  brpprod  36105  brsset  36109  brbigcup  36118  dffix2  36125  elfuns  36135  brimageg  36147  brdomaing  36155  brrangeg  36156  brimg  36157  brapply  36158  lemsuccf  36161  funpartlem  36164  brrestrict  36171  dfrecs2  36172  dfrdg4  36173  brofs  36227  btwncomim  36235  btwnintr  36241  btwnexch3  36242  btwnexch2  36245  brifs  36265  brcolinear2  36280  colineardim1  36283  brfs  36301  btwnconn1  36323  segcon2  36327  seglerflx  36334  seglemin  36335  btwnsegle  36339  colinbtwnle  36340  broutsideof2  36344  fvray  36363  lineunray  36369  lineelsb2  36370  linerflx1  36371  trer  36538  elicc3  36539  finminlem  36540  nn0prpwlem  36544  nn0prpw  36545  fnessref  36579  refssfne  36580  weiunlem  36685  weiunfrlem  36686  weiunfr  36689  weiunse  36690  unblimceq0lem  36734  unblimceq0  36735  unbdqndv2  36739  knoppndvlem21  36760  taupilemrplb  37602  dfgcd3  37606  icorempo  37633  icoreval  37635  iooelexlt  37644  relowlssretop  37645  domalom  37686  ctbssinf  37688  pibt2  37699  phpreu  37884  fin2solem  37886  fin2so  37887  ltflcei  37888  ptrecube  37900  poimirlem1  37901  poimirlem2  37902  poimirlem5  37905  poimirlem6  37906  poimirlem7  37907  poimirlem9  37909  poimirlem12  37912  poimirlem22  37922  poimirlem23  37923  poimirlem24  37924  poimirlem26  37926  poimirlem27  37927  poimirlem32  37932  heicant  37935  mblfinlem1  37937  mblfinlem2  37938  itg2addnclem  37951  itg2addnclem3  37953  itg2addnc  37954  itg2gt0cn  37955  ibladdnclem  37956  iblmulc2nc  37965  itgabsnc  37969  ftc1anclem5  37977  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  indexdom  38014  filbcmb  38020  fdc  38025  prdsbnd  38073  heiborlem3  38093  rrnequiv  38115  rngoueqz  38220  eqbrtr  38518  elrnressn  38560  inxprnres  38578  presucmap  38775  eqvreltr  38971  prtlem10  39270  lsatcveq0  39437  lsatcv1  39453  oposlem  39587  opnlen0  39593  lub0N  39594  glb0N  39598  omllaw  39648  cmtbr4N  39660  cvrval  39674  cvrnbtwn  39676  cvrnbtwn2  39680  cvrnbtwn3  39681  cvrcon3b  39682  cvrnbtwn4  39684  atcvreq0  39719  atnle  39722  atlatmstc  39724  cvlexch1  39733  glbconN  39782  hlsuprexch  39786  exatleN  39809  cvratlem  39826  atcvrj0  39833  atcvrj2b  39837  atlelt  39843  cvrat4  39848  3dim1lem5  39871  3dim2  39873  3dim3  39874  ps-2  39883  llni  39913  llnn0  39921  llnle  39923  lplni  39937  lplni2  39942  lplnle  39945  lplnn0N  39952  llncvrlpln  39963  2llnjN  39972  lvoli  39980  lvoli3  39982  lvoli2  39986  lvoln0N  39996  4at  40018  lplncvrlvol  40021  2lplnj  40025  dalemcea  40065  dalem3  40069  psubspi  40152  linepsubN  40157  elpmap  40163  pmapsub  40173  lnatexN  40184  cdlema1N  40196  cdlemb  40199  elpadd  40204  paddvaln0N  40206  paddasslem5  40229  llnexchb2lem  40273  llnexch2N  40275  islhp  40401  lhpat3  40451  4atexlemex2  40476  4atex  40481  4atex2-0aOLDN  40483  4atex2-0cOLDN  40485  lautle  40489  lautcvr  40497  lauteq  40500  ldilval  40518  ltrnu  40526  trlval2  40568  trlne  40590  cdleme0ex1N  40628  cdleme0nex  40695  cdleme18d  40700  cdlemednuN  40705  cdleme25b  40759  cdleme25cv  40763  cdleme27b  40773  cdleme29b  40780  cdleme31sn  40785  cdleme31fv  40795  cdleme31fv2  40798  cdlemefrs29bpre0  40801  cdlemefr29bpre0N  40811  cdlemefr29clN  40812  cdlemefr32fvaN  40814  cdlemefr32fva1  40815  cdlemefs29pre00N  40817  cdlemefs32sn1aw  40819  cdlemefs29bpre0N  40821  cdlemefs29bpre1N  40822  cdlemefs29cpre1N  40823  cdlemefs29clN  40824  cdlemefs32fvaN  40827  cdlemefs32fva1  40828  cdleme41sn3a  40838  cdleme32fva  40842  cdleme32e  40850  cdleme35f  40859  cdleme40v  40874  cdleme42b  40883  trlord  40974  cdlemg1cex  40993  diaval  41437  diaeldm  41441  diaelrnN  41450  cdlemm10N  41523  dibglbN  41571  dicval  41581  dicfnN  41588  dicvalrelN  41590  dihval  41637  dihlsscpre  41639  dihglblem3N  41700  dihmeetlem2N  41704  djhcvat42  41820  lcmineqlem4  42431  aks4d1p4  42478  aks4d1p5  42479  aks4d1p7  42482  aks4d1p8d2  42484  aks4d1p8  42486  hashnexinjle  42528  sticksstones1  42545  sticksstones2  42546  sticksstones10  42554  sticksstones12a  42556  aks6d1c7lem4  42582  aks6d1c7  42583  grpods  42593  unitscyglem2  42595  unitscyglem3  42596  unitscyglem4  42597  qsalrel  42640  supinf  42641  dvdsexpnn0  42733  redvmptabs  42759  sn-nnne0  42859  sn-sup2  42890  fimgmcyclem  42932  flt4lem2  43034  flt4lem7  43046  lzenom  43156  fphpdo  43203  irrapxlem4  43211  pellexlem6  43220  infmrgelbi  43264  pellfundre  43267  pellfundlb  43270  monotoddzz  43329  zindbi  43332  jm2.27  43394  rmydioph  43400  rpnnen3lem  43417  fnwe2lem2  43437  aomclem8  43447  hbtlem5  43514  hbt  43516  sdomne0  43798  sdomne0d  43799  ensucne0  43914  sucomisnotcard  43929  en2pr  43932  pr2cv  43933  refimssco  43992  rfovfvfvd  44388  rfovcnvf1od  44389  fsovrfovd  44394  nzss  44702  relprel  45336  permaxinf2lem  45397  wessf1ornlem  45573  axccdom  45609  dmrelrnrel  45613  axccd  45616  rnmptlb  45630  rnmptbdd  45632  rnmptbd2  45636  rnmptbdlem  45642  rnmptbd  45643  dstregt0  45673  suplesup  45727  supxrunb3  45786  supxrleubrnmpt  45793  rexabslelem  45805  rexabsle  45806  suprleubrnmpt  45809  infrnmptle  45810  infxrunb3rnmpt  45815  infxrpnf  45833  supminfxr  45851  infrpgernmpt  45852  xrpnf  45872  limsupre  46028  limsupref  46072  limsupbnd1f  46073  limsuppnfd  46089  climinf2  46094  limsuppnf  46098  climinfmpt  46102  climinf3  46103  limsupmnflem  46107  limsupmnf  46108  limsupre2  46112  limsupmnfuzlem  46113  limsupre2mpt  46117  limsupre3lem  46119  limsupre3  46120  limsupre3mpt  46121  limsupre3uzlem  46122  limsupre3uz  46123  limsupreuz  46124  limsupreuzmpt  46126  liminfval2  46155  liminfreuzlem  46189  liminfreuz  46190  xlimpnfxnegmnf  46201  cnrefiisplem  46216  xlimpnfv  46225  xlimpnf  46229  xlimpnfmpt  46231  dfxlim2  46235  icccncfext  46274  cncficcgt0  46275  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  stoweidlem5  46392  stoweidlem20  46407  stoweidlem26  46413  stoweidlem28  46415  stoweidlem29  46416  stoweidlem34  46421  wallispilem3  46454  stirlinglem13  46473  fourierdlem41  46535  fourierdlem42  46536  fourierdlem51  46544  fourierdlem54  46547  salunicl  46703  saluncl  46704  salexct  46721  salexct2  46726  salexct3  46729  salgencntex  46730  salgensscntex  46731  sge0pnffigt  46783  meadjuni  46844  omeunile  46892  ovnlerp  46949  hoidifhspval  46995  ovolval5lem2  47040  salpreimagelt  47094  pimincfltioo  47105  salpreimagtge  47112  salpreimagtlt  47117  incsmf  47129  issmfgt  47143  smfpreimagt  47149  decsmf  47154  issmfge  47157  smfpimgtxr  47167  smfpreimage  47169  smfinflem  47204  smfinf  47205  finfdm  47233  funressnfv  47432  funressnvmo  47434  funressnmo  47435  dfdfat2  47517  tz6.12-afv  47562  funressndmafv2rn  47612  tz6.12-afv2  47629  dfatcolem  47644  dfatco  47645  zplusmodne  47732  m1modne  47737  minusmod5ne  47738  submodneaddmod  47740  modmknepk  47751  iccpartigtl  47812  iccpartgt  47816  icceuelpartlem  47824  iccpartnel  47827  sprsymrelfolem2  47882  goldbachthlem2  47935  odz2prm2pw  47952  fmtnoprmfac1  47954  fmtnoprmfac2  47956  fmtnofac2  47958  fmtno4prmfac  47961  fmtno4prm  47964  prmdvdsfmtnof1lem1  47973  31prm  47986  perfectALTVlem2  48111  nnsum3primes4  48177  nnsum3primesprm  48179  nnsum3primesgbe  48181  nnsum3primesle9  48183  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  wtgoldbnnsum4prm  48191  bgoldbnnsum3prm  48193  bgoldbtbndlem4  48197  bgoldbtbnd  48198  tgblthelfgott  48204  tgoldbach  48206  assintop  48598  isassintop  48599  assintopcllaw  48601  ztprmneprm  48736  ply1mulgsumlem1  48775  ply1mulgsumlem2  48776  lco0  48816  lcoel0  48817  lincsumcl  48820  lincscmcl  48821  lcoss  48825  linindslinci  48837  lindslinindsimp1  48846  linds0  48854  el0ldep  48855  lindsrng01  48857  ldepspr  48862  islindeps2  48872  isldepslvec2  48874  zlmodzxzldep  48893  ldepsnlinc  48897  elbigo2r  48942  xpco2  49245  tposres0  49265  lubsscl  49348  glbsscl  49349  lubprlem  49350  ipolub  49376  ipoglb  49379  catprslem  49398  infsubc2  49449  nelsubc3lem  49458  cnelsubclem  49991  setrec2lem1  50081