Theorem breq1 5100

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

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  breq12  5102  breq1i  5104  breq1d  5107  nbrne2  5117  brab1  5145  pocl  5539  swopolem  5541  swopo  5542  po2ne  5547  solin  5558  sotrieq  5562  sotr2  5565  isso2i  5568  somo  5570  dffr2  5584  frc  5586  frirr  5599  fr2nr  5600  wereu2  5620  vtoclr  5686  frsn  5711  brcog  5814  brcogw  5816  brcnvg  5827  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  6209  coi1  6220  predtrss  6279  frpomin  6297  dffun2  6501  dffun6f  6506  funmo  6507  fun11  6565  fveq2  6833  eliman0  6870  nfunsn  6872  dffv2  6928  fvopab5  6974  dff3  7045  f1ompt  7056  fmptco  7074  dff13  7200  foeqcnvco  7246  isorel  7272  soisores  7273  soisoi  7274  isocnv  7276  isotr  7282  isomin  7283  isoini  7284  isopolem  7291  isosolem  7293  f1oiso  7297  f1oiso2  7298  weniso  7300  eqfunresadj  7306  caovordig  7563  caovordg  7565  caovord3d  7568  caovord  7569  caovord3  7571  caofrss  7661  caoftrn  7663  fr3nr  7717  dfwe2  7719  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  8239  ertr  8651  ecopovsym  8758  ecopovtrn  8759  isfi  8914  en0  8957  en0ALT  8958  en1  8963  endisj  8994  xpcomco  8997  sbth  9027  2pwne  9063  disjenex  9065  ssenen  9081  findcard  9090  findcard2  9091  pssnn  9095  sbthfi  9125  nneneq  9132  php  9133  onomeneq  9140  sdom1  9152  1sdom2dom  9156  isinf  9167  fineqvlem  9168  en1eqsnbi  9178  findcard3  9185  frfi  9187  fiint  9229  mapfienlem1  9310  mapfienlem2  9311  mapfienlem3  9312  mapfien  9313  marypha1lem  9338  supmo  9357  eqsup  9361  supub  9364  suplub  9365  suppr  9377  supisolem  9379  supisoex  9380  infmin  9401  infmo  9402  fiinfg  9406  fiinf2g  9407  infpr  9410  ordtypecbv  9424  ordtypelem3  9427  ordtypelem6  9430  ordtypelem7  9431  ordtypelem9  9433  ordtypelem10  9434  hartogslem1  9449  hartogs  9451  wemaplem1  9453  wemaplem2  9454  wemapso2lem  9459  card2on  9461  card2inf  9462  elharval  9468  brwdom2  9480  wdomtr  9482  cantnfs  9577  cantnfp1lem2  9590  oemapso  9593  cantnflem1  9600  wemapwe  9608  ttrclss  9631  r111  9689  kardex  9808  karden  9809  isnumi  9860  tskwe  9864  cardid2  9867  cardonle  9871  cardne  9879  iscard2  9890  infxpenlem  9925  fodomfi2  9972  wdomfil  9973  wdomnumr  9976  alephsuc2  9992  infenaleph  10003  iunfictbso  10026  infpss  10128  cff1  10170  cfslb2n  10180  sornom  10189  fin4i  10210  isfin6  10212  isfin7  10213  isfin1-3  10298  fin1a2lem9  10320  fin1a2lem11  10322  hsmexlem4  10341  axcc2lem  10348  axcc4dom  10353  domtriomlem  10354  numthcor  10406  zorn2lem2  10409  zorn2lem3  10410  zorn2lem7  10414  zorn2g  10415  axdclem  10431  axdc  10433  brdom7disj  10443  brdom6disj  10444  uniimadom  10456  ondomon  10475  alephval2  10485  alephreg  10495  pwcfsdom  10496  elgch  10535  gchi  10537  fpwwe2lem11  10554  fpwwe2lem12  10555  winainflem  10606  winalim2  10609  tsken  10667  0tsk  10668  inar1  10688  tskord  10693  tskuni  10696  grudomon  10730  pinq  10840  nqereu  10842  enqeq  10847  ltbtwnnq  10891  ltrnq  10892  prcdnq  10906  prnmax  10908  genpnmax  10920  nqpr  10927  1idpr  10942  reclem2pr  10961  reclem3pr  10962  reclem4pr  10963  recexpr  10964  supexpr  10967  ltsosr  11007  1ne0sr  11009  ltasr  11013  supsrlem  11024  axpre-lttri  11078  axpre-lttrn  11079  axpre-ltadd  11080  axpre-sup  11082  lelttr  11225  dedekind  11298  dedekindle  11299  ltordlem  11664  lt0ne0d  11704  fimaxre3  12090  fiminre2  12092  lbreu  12094  lble  12096  sup2  12100  infm3  12103  suprleub  12110  supaddc  12111  supadd  12112  supmul1  12113  supmullem1  12114  supmul  12116  nnne0  12181  nnsub  12191  nominpos  12380  nnunb  12399  arch  12400  nn0sub  12453  nn0n0n1ge2b  12472  nn0lt10b  12556  zextle  12567  peano5uzti  12584  fzind  12592  btwnz  12597  uzval  12755  uzwo  12826  nnwof  12829  ublbneg  12848  lbzbi  12851  zsupss  12852  uzsupss  12855  uzwo3  12858  zmax  12860  rebtwnz  12862  rpnnen1lem3  12894  xrltnsym  13053  xrlttri  13055  xrlttr  13056  xrlelttr  13072  nltpnft  13081  xrmaxlt  13098  xrmaxle  13100  qbtwnre  13116  qbtwnxr  13117  xltnegi  13133  xnn0lenn0nn0  13162  xsubge0  13178  xlesubadd  13180  xmullem2  13182  xlemul1a  13205  xrinfmexpnf  13223  xrsupsslem  13224  xrinfmsslem  13225  xrub  13229  supxrunb1  13236  supxrunb2  13237  reltre  13258  rpltrp  13259  reltxrnmnf  13260  ixxval  13271  elixx1  13272  elioo2  13304  iccid  13308  icc0  13311  fzval  13427  elfz1  13430  elfznelfzo  13691  elfznelfzob  13692  flval  13716  fllelt  13719  flflp1  13729  flval2  13736  flval3  13737  flbi  13738  dfceil2  13761  ceilval2  13762  fleqceilz  13776  modid2  13820  addmodlteq  13871  fsequb2  13901  ssnn0fi  13910  seqf1olem2  13967  sqlecan  14134  faclbnd4lem1  14218  hashsnle1  14342  pr2pwpr  14404  hash3tpde  14418  rtrclreclem3  14985  relexpindlem  14988  sgnval  15013  01sqrexlem6  15172  01sqrex  15174  abslt  15240  absle  15241  rexanre  15272  rexico  15279  limsupgle  15402  limsupgre  15406  limsupbnd2  15408  rlim2lt  15422  rlim3  15423  ello12r  15442  ello1d  15448  elo12r  15453  rlimconst  15469  climshft  15501  rlimcn3  15515  o1rlimmul  15544  lo1le  15577  climsup  15595  caucvgrlem  15598  isumless  15770  divrcnv  15777  cvgrat  15808  rpnnen2lem10  16150  ruclem1  16158  ruclem2  16159  ruclem11  16167  ruclem12  16168  sqrt2irr  16176  absdvdsb  16203  dvdsle  16239  dvdsabseq  16242  dvdsdivcl  16245  dvdsext  16250  divalglem8  16329  divalglem9  16330  divalglem10  16331  divalgmod  16335  ndvdssub  16338  sadcaddlem  16386  gcdcllem1  16428  gcdcllem2  16429  gcdcllem3  16430  dfgcd2  16475  gcdzeq  16481  dvdssq  16496  nn0seqcvgd  16499  algcvgblem  16506  lcmval  16521  lcmdvds  16537  lcmgcdeq  16541  lcmfpr  16556  lcmf  16562  lcmftp  16565  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  lcmfdvdsb  16572  coprmgcdb  16578  coprmdvds1  16581  1nprm  16608  1idssfct  16609  isprm2lem  16610  isprm2  16611  dvdsprime  16616  nprm  16617  3prm  16623  dvdsprm  16632  exprmfct  16633  isprm5  16636  maxprmfct  16638  coprm  16640  prmdvdsncoprmbd  16656  ncoprmlnprm  16657  eulerthlem2  16711  phisum  16720  odzval  16721  pythagtriplem4  16749  pc2dvds  16809  pcprmpw2  16812  pcprmpw  16813  dvdsprmpweqle  16816  oddprmdvds  16833  prmpwdvds  16834  pockthg  16836  unbenlem  16838  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  1arith  16857  vdwlem6  16916  vdwlem11  16921  vdwlem13  16923  ramtlecl  16930  ramub  16943  rami  16945  ramubcl  16948  0ram  16950  ram0  16952  prmdvdsprmop  16973  prmolefac  16976  prmodvdslcmf  16977  prmgaplem2  16980  prmgaplcmlem1  16981  prmgaplcmlem2  16982  prmgaplem3  16983  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  prmgapprmolem  16991  prmlem0  17035  prmlem1a  17036  imasaddfnlem  17451  imasvscafn  17460  imasleval  17464  prslem  18222  drsdir  18227  drsdirfi  18230  isdrs2  18231  posi  18242  posasymb  18244  pospropd  18250  pltval3  18262  plelttr  18267  pospo  18268  lubprop  18281  luble  18282  lublecllem  18283  glbprop  18294  joinval2lem  18303  joinlem  18306  meetlem  18320  meetle  18323  poslubmo  18334  posglbmo  18335  poslubd  18336  tleile  18344  latnlej  18381  isglbd  18434  lubub  18436  lubun  18440  clatleglb  18443  tsrlin  18510  letsr  18518  dirge  18528  pmtrval  19382  pmtrrn  19388  pmtrfrn  19389  pmtrrn2  19391  pmtrsn  19450  mndodcongi  19474  odeq  19481  odmulgeq  19488  gexnnod  19519  sylow1lem1  19529  pgpssslw  19545  sylow2a  19550  efgredeu  19683  efgred2  19684  gexex  19784  frgpnabllem2  19805  cyggenod  19815  dprdval  19936  dprdw  19943  dprdwd  19944  ablfacrplem  19998  ablfac1c  20004  ablfac1eu  20006  ablfaclem3  20020  omndadd  20059  abvtrivd  20767  zringlpir  21424  prmirredlem  21429  znleval  21511  frlmelbas  21713  ellspd  21759  islindf4  21795  psrbagconcl  21885  psrbagleadd1  21886  gsumbagdiaglem  21888  rhmpsrlem2  21899  psrlidm  21919  psrridm  21920  psrass1  21921  psrcom  21925  mplelbas  21948  mplmonmul  21993  ltbwe  22001  mhpmulcl  22094  psdmul  22111  coe1fsupp  22157  coe1ae0  22159  coe1mul2  22213  coe1tmmul  22221  pmatcoe1fsupp  22647  chfacffsupp  22802  chfacfscmulfsupp  22805  chfacfscmulgsum  22806  chfacfpmmulfsupp  22809  chfacfpmmulgsum  22810  ordtbas2  23137  ordtopn2  23141  ordtrest2lem  23149  pnfnei  23166  ordtt1  23325  ordthauslem  23329  2ndci  23394  2ndcsb  23395  2ndcredom  23396  2ndc1stc  23397  1stcrest  23399  2ndcctbss  23401  2ndcdisj  23402  2ndcsep  23405  lly1stc  23442  tx1stc  23596  ordthmeolem  23747  ufildom1  23872  xmetrtri2  24302  prdsxmetlem  24314  ssblex  24374  prdsbl  24437  comet  24459  stdbdxmet  24461  stdbdmopn  24464  met1stc  24467  dscmet  24518  metdstri  24798  metdscn  24803  xrhmeo  24902  bndth  24915  evth  24916  lebnumlem3  24920  pcovalg  24970  pco1  24973  pcocn  24975  pcopt  24980  pcopt2  24981  pcoass  24982  nmoleub3  25077  bcthlem5  25286  rrxfsupp  25360  minveclem4c  25383  minveclem2  25384  minveclem3b  25386  minveclem4  25390  minveclem6  25392  pmltpclem1  25407  pmltpc  25409  ovollb2lem  25447  ovolctb  25449  ovolunlem1  25456  ovoliunlem1  25461  ovoliunlem2  25462  ovoliun2  25465  ovolshftlem1  25468  ovolscalem1  25472  ovolicc1  25475  ovolicc2lem3  25478  voliunlem2  25510  voliunlem3  25511  ioombl1lem4  25520  uniioovol  25538  uniioombllem2  25542  uniioombllem3  25544  uniioombllem6  25547  volsup2  25564  ismbfd  25598  mbfsup  25623  mbflimsup  25625  itg1climres  25673  mbfi1fseqlem4  25677  itg2lr  25689  itg2leub  25693  itg2seq  25701  itg2monolem1  25709  itg2monolem3  25711  itg2mono  25712  itg2i1fseq2  25715  itg2gt0  25719  itg2cnlem1  25720  itg2cnlem2  25721  itg2cn  25722  iblss  25764  itgless  25776  ibladdlem  25779  iblabsr  25789  iblmulc2  25790  itgabs  25794  bddiblnc  25801  ditgeq1  25807  dvferm2lem  25948  rolle  25952  dvlip2  25958  c1liplem1  25959  c1lip1  25960  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem4  25994  mdegleb  26027  degltlem1  26035  plyco0  26155  plyeq0lem  26173  coeeq2  26205  dgrle  26206  dgradd2  26232  plydiveu  26264  aareccl  26292  aalioulem2  26299  aaliou3lem7  26315  psercnlem1  26393  pilem2  26420  pilem3  26421  logltb  26567  divlogrlim  26602  logcnlem3  26611  cxpaddlelem  26719  rlimcnp  26933  cxplim  26940  cxploglim  26946  scvxcvx  26954  ftalem1  27041  ftalem2  27042  isppw2  27083  vmappw  27084  sgmnncl  27115  sqff1o  27150  fsumdvdsdiaglem  27151  dvdsppwf1o  27154  dvdsflsumcom  27156  musum  27159  muinv  27161  mpodvdsmulf1o  27162  dvdsmulf1o  27164  vmalelog  27174  vmasum  27185  logfac2  27186  perfectlem2  27199  bcmono  27246  bpos1lem  27251  bposlem9  27261  lgsmod  27292  lgsne0  27304  gausslemma2dlem4  27338  2sqlem6  27392  2sqlem8  27395  2sqlem10  27397  2sqreulem1  27415  2sqreunnlem1  27418  chtppilim  27444  rpvmasumlem  27456  dchrisumlema  27457  dchrisumlem2  27459  dchrvmasumlem1  27464  dchrvmasumiflem1  27470  dchrisum0flblem1  27477  dchrisum0flblem2  27478  dchrisum0  27489  rplogsum  27496  logsqvma  27511  pntpbnd1  27555  pntpbnd2  27556  pntibndlem3  27561  pntlemj  27572  pntlemi  27573  pntlem3  27578  pnt3  27581  ostth3  27607  nodense  27662  noresle  27667  nosupprefixmo  27670  noinfprefixmo  27671  nosupcbv  27672  nosupdm  27674  nosupbnd1lem1  27678  nosupbnd1lem4  27681  nosupbnd1  27684  nosupbnd2lem1  27685  nosupbnd2  27686  noinfcbv  27687  noinfdm  27689  noinffv  27691  noinfres  27692  noinfbnd1lem3  27695  noinfbnd1lem4  27696  noinfbnd1lem5  27697  noinfbnd1  27699  noetalem2  27712  nocvxminlem  27752  ssltsnb  27767  ssltsepc  27769  conway  27775  scutval  27776  etasslt  27789  slerec  27795  eqscut3  27800  bday1s  27810  cuteq1  27813  madeval2  27829  rightval  27840  elleft  27841  ssltright  27851  made0  27853  madecut  27863  left1s  27875  madebdaylemlrcut  27879  sltlpss  27888  cofsslt  27898  coinitsslt  27899  cofcutr  27904  cofcutrtime  27907  cofss  27910  coiniss  27911  cutmax  27914  cutmin  27915  cutminmax  27916  addsproplem1  27949  addsprop  27956  sleadd1  27969  addsuniflem  27981  negsproplem1  28008  negsprop  28015  negsid  28021  negsunif  28035  mulsproplemcbv  28095  mulsproplem1  28096  mulsproplem9  28104  mulsprop  28110  ssltmul1  28127  ssltmul2  28128  mulsuniflem  28129  precsexlem11  28196  absslt  28228  onscutlt  28243  onsiso  28250  bdayon  28255  addsonbday  28258  n0sfincut  28333  onsfi  28334  n0subs  28340  bdayn0p1  28346  eucliddivs  28353  zscut  28384  twocut  28400  halfcut  28435  addhalfcut  28436  bdaypw2n0sbndlem  28440  bdayfinbndcbv  28443  bdayfinbndlem1  28444  bdayfinbndlem2  28445  zs12bdaylem1  28447  elreno  28468  elreno2  28472  tgjustc1  28528  tgjustc2  28529  iscgrglt  28567  tgcgr4  28584  hlcgreu  28671  lmif  28838  islmib  28840  trgcopyeu  28859  iscgrad  28864  inaghl  28898  axlowdim2  29014  axlowdim  29015  axcontlem2  29019  axcontlem3  29020  axcontlem4  29021  axcontlem7  29024  axcontlem9  29026  axcontlem10  29027  axcontlem11  29028  axcontlem12  29029  ebtwntg  29036  umgrupgr  29157  nbusgrvtxm1  29433  crctcshwlkn0lem2  29865  crctcshwlkn0lem3  29866  crctcsh  29878  wlkswwlksf1o  29933  clwlkclwwlklem2fv1  30051  clwlkclwwlkf  30064  0clwlkv  30187  eupth2  30295  numclwwlk5  30444  nmoubi  30828  minvecolem2  30931  minvecolem3  30932  minvecolem4c  30935  minvecolem4  30936  minvecolem5  30937  minvecolem6  30938  htthlem  30973  chlimi  31290  chcompl  31298  hsn0elch  31304  cmbr3  31664  cmcm  31670  cmcm3  31671  lecm  31673  nmopub  31964  nmfnleub  31981  nmopun  32070  nmcexi  32082  cnlnadjlem7  32129  pjnmopi  32204  stle0i  32295  stlesi  32297  stm1i  32299  csmdsymi  32390  cvmd  32392  atcveq0  32404  atcv1  32436  atord  32444  atcvat2  32445  chirred  32451  mdsym  32468  mddmdin0i  32487  cdj1i  32489  fmptcof2  32715  fnpreimac  32728  isoun  32760  fcobijfs  32779  fcobijfs2  32780  lt2addrd  32809  xlt2addrd  32818  xrge0infss  32819  infxrge0glb  32824  xrofsup  32826  fz1nnct  32860  sgnmulsgn  32902  toslublem  33033  tosglblem  33035  ismntd  33045  mgccole1  33051  mgccole2  33052  mgcmnt1  33053  mgcmnt2  33054  dfmgc2lem  33056  dfmgc2  33057  psgnfzto1stlem  33161  fzto1st  33164  psgnfzto1st  33166  trsp2cyc  33184  xrnarchi  33245  archirng  33249  archiexdiv  33251  archiabl  33259  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  linds2eq  33441  elrspunidl  33488  elrspunsn  33489  isrprm  33577  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  extvfvvcl  33679  extvfvcl  33680  mplmulmvr  33683  evlextv  33686  mplvrpmlem  33687  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  esplyfval0  33701  esplylem  33703  esplyfv1  33706  esplyfval3  33709  esplyind  33710  ply1degltdimlem  33758  lbsdiflsp0  33762  fedgmullem1  33765  fedgmullem2  33766  fedgmul  33767  fldextrspunlsplem  33809  fldextrspunlsp  33810  smatrcl  33932  smatlem  33933  madjusmdetlem2  33964  madjusmdet  33967  cmpcref  33986  ldlfcntref  33990  dispcmp  33995  zarcmplem  34017  ordtrest2NEWlem  34058  ordtconnlem1  34060  xrge0iifiso  34071  rge0scvg  34085  gsumesum  34195  esumfsup  34206  esumpinfval  34209  esumpcvgval  34214  esumcvg  34222  sigaclcu  34253  sigaclci  34268  unelsiga  34270  unelldsys  34294  sigapildsys  34298  ldgenpisyslem1  34299  fiunelros  34310  measvun  34345  voliune  34365  volfiniune  34366  oms0  34433  omssubaddlem  34435  omssubadd  34436  carsgsigalem  34451  carsgclctunlem2  34455  carsgclctun  34457  pmeasmono  34460  pmeasadd  34461  orvcval2  34595  dstfrvel  34610  ballotlemfc0  34629  ballotlemfcc  34630  ballotlemsv  34646  ballotlemsf1o  34650  breprexp  34769  tgoldbachgt  34799  bnj23  34853  bnj1185  34928  bnj1152  35133  bnj1418  35175  fnrelpredd  35226  loop1cycl  35310  umgr2cycl  35314  acycgrcycl  35320  dfdm5  35946  dfrn5  35947  wzel  35995  wsuclem  35996  brpprod  36056  brsset  36060  brbigcup  36069  dffix2  36076  elfuns  36086  brimageg  36098  brdomaing  36106  brrangeg  36107  brimg  36108  brapply  36109  lemsuccf  36112  funpartlem  36115  brrestrict  36122  dfrecs2  36123  dfrdg4  36124  brofs  36178  btwncomim  36186  btwnintr  36192  btwnexch3  36193  btwnexch2  36196  brifs  36216  brcolinear2  36231  colineardim1  36234  brfs  36252  btwnconn1  36274  segcon2  36278  seglerflx  36285  seglemin  36286  btwnsegle  36290  colinbtwnle  36291  broutsideof2  36295  fvray  36314  lineunray  36320  lineelsb2  36321  linerflx1  36322  trer  36489  elicc3  36490  finminlem  36491  nn0prpwlem  36495  nn0prpw  36496  fnessref  36530  refssfne  36531  weiunlem2  36636  weiunfrlem  36637  weiunfr  36640  weiunse  36641  unblimceq0lem  36679  unblimceq0  36680  unbdqndv2  36684  knoppndvlem21  36705  taupilemrplb  37494  dfgcd3  37498  icorempo  37525  icoreval  37527  iooelexlt  37536  relowlssretop  37537  domalom  37578  ctbssinf  37580  pibt2  37591  phpreu  37774  fin2solem  37776  fin2so  37777  ltflcei  37778  ptrecube  37790  poimirlem1  37791  poimirlem2  37792  poimirlem5  37795  poimirlem6  37796  poimirlem7  37797  poimirlem9  37799  poimirlem12  37802  poimirlem22  37812  poimirlem23  37813  poimirlem24  37814  poimirlem26  37816  poimirlem27  37817  poimirlem32  37822  heicant  37825  mblfinlem1  37827  mblfinlem2  37828  itg2addnclem  37841  itg2addnclem3  37843  itg2addnc  37844  itg2gt0cn  37845  ibladdnclem  37846  iblmulc2nc  37855  itgabsnc  37859  ftc1anclem5  37867  ftc1anclem7  37869  ftc1anclem8  37870  ftc1anc  37871  indexdom  37904  filbcmb  37910  fdc  37915  prdsbnd  37963  heiborlem3  37983  rrnequiv  38005  rngoueqz  38110  eqbrtr  38408  elrnressn  38450  inxprnres  38468  presucmap  38665  eqvreltr  38861  prtlem10  39160  lsatcveq0  39327  lsatcv1  39343  oposlem  39477  opnlen0  39483  lub0N  39484  glb0N  39488  omllaw  39538  cmtbr4N  39550  cvrval  39564  cvrnbtwn  39566  cvrnbtwn2  39570  cvrnbtwn3  39571  cvrcon3b  39572  cvrnbtwn4  39574  atcvreq0  39609  atnle  39612  atlatmstc  39614  cvlexch1  39623  glbconN  39672  hlsuprexch  39676  exatleN  39699  cvratlem  39716  atcvrj0  39723  atcvrj2b  39727  atlelt  39733  cvrat4  39738  3dim1lem5  39761  3dim2  39763  3dim3  39764  ps-2  39773  llni  39803  llnn0  39811  llnle  39813  lplni  39827  lplni2  39832  lplnle  39835  lplnn0N  39842  llncvrlpln  39853  2llnjN  39862  lvoli  39870  lvoli3  39872  lvoli2  39876  lvoln0N  39886  4at  39908  lplncvrlvol  39911  2lplnj  39915  dalemcea  39955  dalem3  39959  psubspi  40042  linepsubN  40047  elpmap  40053  pmapsub  40063  lnatexN  40074  cdlema1N  40086  cdlemb  40089  elpadd  40094  paddvaln0N  40096  paddasslem5  40119  llnexchb2lem  40163  llnexch2N  40165  islhp  40291  lhpat3  40341  4atexlemex2  40366  4atex  40371  4atex2-0aOLDN  40373  4atex2-0cOLDN  40375  lautle  40379  lautcvr  40387  lauteq  40390  ldilval  40408  ltrnu  40416  trlval2  40458  trlne  40480  cdleme0ex1N  40518  cdleme0nex  40585  cdleme18d  40590  cdlemednuN  40595  cdleme25b  40649  cdleme25cv  40653  cdleme27b  40663  cdleme29b  40670  cdleme31sn  40675  cdleme31fv  40685  cdleme31fv2  40688  cdlemefrs29bpre0  40691  cdlemefr29bpre0N  40701  cdlemefr29clN  40702  cdlemefr32fvaN  40704  cdlemefr32fva1  40705  cdlemefs29pre00N  40707  cdlemefs32sn1aw  40709  cdlemefs29bpre0N  40711  cdlemefs29bpre1N  40712  cdlemefs29cpre1N  40713  cdlemefs29clN  40714  cdlemefs32fvaN  40717  cdlemefs32fva1  40718  cdleme41sn3a  40728  cdleme32fva  40732  cdleme32e  40740  cdleme35f  40749  cdleme40v  40764  cdleme42b  40773  trlord  40864  cdlemg1cex  40883  diaval  41327  diaeldm  41331  diaelrnN  41340  cdlemm10N  41413  dibglbN  41461  dicval  41471  dicfnN  41478  dicvalrelN  41480  dihval  41527  dihlsscpre  41529  dihglblem3N  41590  dihmeetlem2N  41594  djhcvat42  41710  lcmineqlem4  42321  aks4d1p4  42368  aks4d1p5  42369  aks4d1p7  42372  aks4d1p8d2  42374  aks4d1p8  42376  hashnexinjle  42418  sticksstones1  42435  sticksstones2  42436  sticksstones10  42444  sticksstones12a  42446  aks6d1c7lem4  42472  aks6d1c7  42473  grpods  42483  unitscyglem2  42485  unitscyglem3  42486  unitscyglem4  42487  qsalrel  42533  supinf  42534  dvdsexpnn0  42626  redvmptabs  42652  sn-nnne0  42752  sn-sup2  42783  fimgmcyclem  42825  flt4lem2  42927  flt4lem7  42939  lzenom  43049  fphpdo  43096  irrapxlem4  43104  pellexlem6  43113  infmrgelbi  43157  pellfundre  43160  pellfundlb  43163  monotoddzz  43222  zindbi  43225  jm2.27  43287  rmydioph  43293  rpnnen3lem  43310  fnwe2lem2  43330  aomclem8  43340  hbtlem5  43407  hbt  43409  sdomne0  43691  sdomne0d  43692  ensucne0  43807  sucomisnotcard  43822  en2pr  43825  pr2cv  43826  refimssco  43885  rfovfvfvd  44281  rfovcnvf1od  44282  fsovrfovd  44287  nzss  44595  relprel  45229  permaxinf2lem  45290  wessf1ornlem  45466  axccdom  45503  dmrelrnrel  45507  axccd  45510  rnmptlb  45524  rnmptbdd  45526  rnmptbd2  45530  rnmptbdlem  45536  rnmptbd  45537  dstregt0  45567  suplesup  45621  supxrunb3  45680  supxrleubrnmpt  45687  rexabslelem  45699  rexabsle  45700  suprleubrnmpt  45703  infrnmptle  45704  infxrunb3rnmpt  45709  infxrpnf  45727  supminfxr  45745  infrpgernmpt  45746  xrpnf  45766  limsupre  45922  limsupref  45966  limsupbnd1f  45967  limsuppnfd  45983  climinf2  45988  limsuppnf  45992  climinfmpt  45996  climinf3  45997  limsupmnflem  46001  limsupmnf  46002  limsupre2  46006  limsupmnfuzlem  46007  limsupre2mpt  46011  limsupre3lem  46013  limsupre3  46014  limsupre3mpt  46015  limsupre3uzlem  46016  limsupre3uz  46017  limsupreuz  46018  limsupreuzmpt  46020  liminfval2  46049  liminfreuzlem  46083  liminfreuz  46084  xlimpnfxnegmnf  46095  cnrefiisplem  46110  xlimpnfv  46119  xlimpnf  46123  xlimpnfmpt  46125  dfxlim2  46129  icccncfext  46168  cncficcgt0  46169  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  stoweidlem5  46286  stoweidlem20  46301  stoweidlem26  46307  stoweidlem28  46309  stoweidlem29  46310  stoweidlem34  46315  wallispilem3  46348  stirlinglem13  46367  fourierdlem41  46429  fourierdlem42  46430  fourierdlem51  46438  fourierdlem54  46441  salunicl  46597  saluncl  46598  salexct  46615  salexct2  46620  salexct3  46623  salgencntex  46624  salgensscntex  46625  sge0pnffigt  46677  meadjuni  46738  omeunile  46786  ovnlerp  46843  hoidifhspval  46889  ovolval5lem2  46934  salpreimagelt  46988  pimincfltioo  46999  salpreimagtge  47006  salpreimagtlt  47011  incsmf  47023  issmfgt  47037  smfpreimagt  47043  decsmf  47048  issmfge  47051  smfpimgtxr  47061  smfpreimage  47063  smfinflem  47098  smfinf  47099  finfdm  47127  funressnfv  47326  funressnvmo  47328  funressnmo  47329  dfdfat2  47411  tz6.12-afv  47456  funressndmafv2rn  47506  tz6.12-afv2  47523  dfatcolem  47538  dfatco  47539  zplusmodne  47626  m1modne  47631  minusmod5ne  47632  submodneaddmod  47634  modmknepk  47645  iccpartigtl  47706  iccpartgt  47710  icceuelpartlem  47718  iccpartnel  47721  sprsymrelfolem2  47776  goldbachthlem2  47829  odz2prm2pw  47846  fmtnoprmfac1  47848  fmtnoprmfac2  47850  fmtnofac2  47852  fmtno4prmfac  47855  fmtno4prm  47858  prmdvdsfmtnof1lem1  47867  31prm  47880  perfectALTVlem2  48005  nnsum3primes4  48071  nnsum3primesprm  48073  nnsum3primesgbe  48075  nnsum3primesle9  48077  nnsum4primeseven  48083  nnsum4primesevenALTV  48084  wtgoldbnnsum4prm  48085  bgoldbnnsum3prm  48087  bgoldbtbndlem4  48091  bgoldbtbnd  48092  tgblthelfgott  48098  tgoldbach  48100  assintop  48492  isassintop  48493  assintopcllaw  48495  ztprmneprm  48630  ply1mulgsumlem1  48669  ply1mulgsumlem2  48670  lco0  48710  lcoel0  48711  lincsumcl  48714  lincscmcl  48715  lcoss  48719  linindslinci  48731  lindslinindsimp1  48740  linds0  48748  el0ldep  48749  lindsrng01  48751  ldepspr  48756  islindeps2  48766  isldepslvec2  48768  zlmodzxzldep  48787  ldepsnlinc  48791  elbigo2r  48836  xpco2  49139  tposres0  49159  lubsscl  49242  glbsscl  49243  lubprlem  49244  ipolub  49270  ipoglb  49273  catprslem  49292  infsubc2  49343  nelsubc3lem  49352  cnelsubclem  49885  setrec2lem1  49975