Theorem breq1 5073

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  breq12  5075  breq1i  5077  breq1d  5080  nbrne2  5090  brab1  5118  pocl  5501  poclOLD  5502  swopolem  5504  swopo  5505  po2ne  5510  solin  5519  sotrieq  5523  sotr2  5526  isso2i  5529  somo  5531  dffr2  5544  frc  5546  frirr  5557  fr2nr  5558  wereu2  5577  vtoclr  5641  frsn  5665  brcog  5764  brcogw  5766  brcnvg  5777  dfdmf  5794  eldmg  5796  dfrnf  5848  dfres2  5938  imasng  5980  asymref2  6011  sotri2  6023  somin1  6027  coi1  6155  predtrss  6214  frpomin  6228  dffun6f  6432  funmo  6434  fun11  6492  fveq2  6756  eliman0  6791  nfunsn  6793  dffv2  6845  fvopab5  6889  dff3  6958  f1ompt  6967  fmptco  6983  dff13  7109  foeqcnvco  7152  isorel  7177  soisores  7178  soisoi  7179  isocnv  7181  isotr  7187  isomin  7188  isoini  7189  isopolem  7196  isosolem  7198  f1oiso  7202  f1oiso2  7203  weniso  7205  caovordig  7455  caovordg  7457  caovord3d  7460  caovord  7461  caovord3  7463  caofrss  7547  caoftrn  7549  fr3nr  7600  dfwe2  7602  f1oweALT  7788  frxp  7938  poxp  7940  fnse  7945  brtpos2  8019  rntpos  8026  tpostpos  8033  frrlem12  8084  ertr  8471  ecopovsym  8566  ecopovtrn  8567  isfi  8719  en0  8758  en0OLD  8759  en0ALT  8760  en1  8765  en1OLD  8766  endisj  8799  xpcomco  8802  sbth  8833  2pwne  8869  disjenex  8871  ssenen  8887  nneneq  8896  php  8897  findcard  8908  findcard2  8909  pssnn  8913  sbthfi  8942  sdom1  8952  isinf  8965  fineqvlem  8966  pssnnOLD  8969  en1eqsnbi  8978  enp1i  8982  findcard2OLD  8986  findcard3  8987  frfi  8989  fiint  9021  mapfienlem1  9094  mapfienlem2  9095  mapfienlem3  9096  mapfien  9097  marypha1lem  9122  supmo  9141  eqsup  9145  supub  9148  suplub  9149  suppr  9160  supisolem  9162  supisoex  9163  infmin  9183  infmo  9184  fiinfg  9188  fiinf2g  9189  infpr  9192  ordtypecbv  9206  ordtypelem3  9209  ordtypelem6  9212  ordtypelem7  9213  ordtypelem9  9215  ordtypelem10  9216  hartogslem1  9231  hartogs  9233  wemaplem1  9235  wemaplem2  9236  wemapso2lem  9241  card2on  9243  card2inf  9244  elharval  9250  brwdom2  9262  wdomtr  9264  cantnfs  9354  cantnfp1lem2  9367  oemapso  9370  cantnflem1  9377  wemapwe  9385  trpredpred  9406  r111  9464  kardex  9583  karden  9584  isnumi  9635  tskwe  9639  cardid2  9642  cardonle  9646  cardne  9654  iscard2  9665  infxpenlem  9700  fodomfi2  9747  wdomfil  9748  wdomnumr  9751  alephsuc2  9767  infenaleph  9778  iunfictbso  9801  infpss  9904  cff1  9945  cfslb2n  9955  sornom  9964  fin4i  9985  isfin6  9987  isfin7  9988  isfin1-3  10073  fin1a2lem9  10095  fin1a2lem11  10097  hsmexlem4  10116  axcc2lem  10123  axcc4dom  10128  domtriomlem  10129  numthcor  10181  zorn2lem2  10184  zorn2lem3  10185  zorn2lem7  10189  zorn2g  10190  axdclem  10206  axdc  10208  brdom7disj  10218  brdom6disj  10219  uniimadom  10231  ondomon  10250  alephval2  10259  alephreg  10269  pwcfsdom  10270  elgch  10309  gchi  10311  fpwwe2lem11  10328  fpwwe2lem12  10329  pwfseqlem4  10349  winainflem  10380  winalim2  10383  tsken  10441  0tsk  10442  inar1  10462  tskord  10467  tskuni  10470  grudomon  10504  pinq  10614  nqereu  10616  enqeq  10621  ltbtwnnq  10665  ltrnq  10666  prcdnq  10680  prnmax  10682  genpnmax  10694  nqpr  10701  1idpr  10716  reclem2pr  10735  reclem3pr  10736  reclem4pr  10737  recexpr  10738  supexpr  10741  ltsosr  10781  1ne0sr  10783  ltasr  10787  supsrlem  10798  axpre-lttri  10852  axpre-lttrn  10853  axpre-ltadd  10854  axpre-sup  10856  lelttr  10996  dedekind  11068  dedekindle  11069  ltordlem  11430  lt0ne0d  11470  fimaxre3  11851  fiminre2  11853  lbreu  11855  lble  11857  sup2  11861  infm3  11864  suprleub  11871  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmul  11877  nnne0  11937  nnsub  11947  nominpos  12140  nnunb  12159  arch  12160  nn0sub  12213  nn0n0n1ge2b  12231  nn0lt10b  12312  zextle  12323  peano5uzti  12340  fzind  12348  btwnz  12352  uzval  12513  uzwo  12580  nnwof  12583  ublbneg  12602  lbzbi  12605  zsupss  12606  uzsupss  12609  uzwo3  12612  zmax  12614  rebtwnz  12616  rpnnen1lem3  12648  xrltnsym  12800  xrlttri  12802  xrlttr  12803  xrlelttr  12819  nltpnft  12827  xrmaxlt  12844  xrmaxle  12846  qbtwnre  12862  qbtwnxr  12863  xltnegi  12879  xnn0lenn0nn0  12908  xsubge0  12924  xlesubadd  12926  xmullem2  12928  xlemul1a  12951  xrinfmexpnf  12969  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  supxrunb1  12982  supxrunb2  12983  reltre  13003  rpltrp  13004  reltxrnmnf  13005  ixxval  13016  elixx1  13017  elioo2  13049  iccid  13053  icc0  13056  fzval  13170  elfz1  13173  elfznelfzo  13420  elfznelfzob  13421  flval  13442  fllelt  13445  flflp1  13455  flval2  13462  flval3  13463  flbi  13464  dfceil2  13487  ceilval2  13488  fleqceilz  13502  modid2  13546  addmodlteq  13594  fsequb2  13624  ssnn0fi  13633  seqf1olem2  13691  sqlecan  13853  faclbnd4lem1  13935  hashsnle1  14060  pr2pwpr  14121  rtrclreclem3  14699  relexpindlem  14702  sgnval  14727  sqrlem6  14887  01sqrex  14889  abslt  14954  absle  14955  rexanre  14986  rexico  14993  limsupgle  15114  limsupgre  15118  limsupbnd2  15120  rlim2lt  15134  rlim3  15135  ello12r  15154  ello1d  15160  elo12r  15165  rlimconst  15181  climshft  15213  rlimcn3  15227  o1rlimmul  15256  lo1le  15291  climsup  15309  caucvgrlem  15312  isumless  15485  divrcnv  15492  cvgrat  15523  rpnnen2lem10  15860  ruclem1  15868  ruclem2  15869  ruclem11  15877  ruclem12  15878  sqrt2irr  15886  absdvdsb  15912  dvdsle  15947  dvdsabseq  15950  dvdsdivcl  15953  dvdsext  15958  divalglem8  16037  divalglem9  16038  divalglem10  16039  divalgmod  16043  ndvdssub  16046  sadcaddlem  16092  gcdcllem1  16134  gcdcllem2  16135  gcdcllem3  16136  dfgcd2  16182  gcdzeq  16190  dvdssq  16200  nn0seqcvgd  16203  algcvgblem  16210  lcmval  16225  lcmdvds  16241  lcmgcdeq  16245  lcmfpr  16260  lcmf  16266  lcmftp  16269  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfdvdsb  16276  coprmgcdb  16282  coprmdvds1  16285  1nprm  16312  1idssfct  16313  isprm2lem  16314  isprm2  16315  dvdsprime  16320  nprm  16321  3prm  16327  dvdsprm  16336  exprmfct  16337  isprm5  16340  maxprmfct  16342  coprm  16344  prmdvdsncoprmbd  16359  ncoprmlnprm  16360  eulerthlem2  16411  phisum  16419  odzval  16420  pythagtriplem4  16448  pc2dvds  16508  pcprmpw2  16511  pcprmpw  16512  dvdsprmpweqle  16515  oddprmdvds  16532  prmpwdvds  16533  pockthg  16535  unbenlem  16537  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  1arith  16556  vdwlem6  16615  vdwlem11  16620  vdwlem13  16622  ramtlecl  16629  ramub  16642  rami  16644  ramubcl  16647  0ram  16649  ram0  16651  prmdvdsprmop  16672  prmolefac  16675  prmodvdslcmf  16676  prmgaplem2  16679  prmgaplcmlem1  16680  prmgaplcmlem2  16681  prmgaplem3  16682  prmgaplem4  16683  prmgaplem5  16684  prmgaplem6  16685  prmgapprmolem  16690  prmlem0  16735  prmlem1a  16736  imasaddfnlem  17156  imasvscafn  17165  imasleval  17169  prslem  17931  drsdir  17935  drsdirfi  17938  isdrs2  17939  posi  17950  posasymb  17952  pospropd  17960  pltval3  17972  plelttr  17977  pospo  17978  lubprop  17991  luble  17992  lublecllem  17993  glbprop  18004  joinval2lem  18013  joinlem  18016  meetlem  18030  meetle  18033  poslubmo  18044  posglbmo  18045  poslubd  18046  tleile  18054  latnlej  18089  isglbd  18142  lubub  18144  lubun  18148  clatleglb  18151  tsrlin  18218  letsr  18226  dirge  18236  pmtrval  18974  pmtrrn  18980  pmtrfrn  18981  pmtrrn2  18983  pmtrsn  19042  mndodcongi  19066  odeq  19073  odmulgeq  19079  gexnnod  19108  sylow1lem1  19118  pgpssslw  19134  sylow2a  19139  efgredeu  19273  efgred2  19274  gexex  19369  frgpnabllem2  19390  cyggenod  19399  dprdval  19521  dprdw  19528  dprdwd  19529  ablfacrplem  19583  ablfac1c  19589  ablfac1eu  19591  ablfaclem3  19605  abvtrivd  20015  zringlpir  20601  prmirredlem  20606  znleval  20674  frlmelbas  20873  ellspd  20919  islindf4  20955  psrbagconcl  21047  psrbagconclOLD  21048  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  psrmulcllem  21066  psrlidm  21082  psrridm  21083  psrass1  21084  psrcom  21088  mplelbas  21109  mplmonmul  21147  ltbwe  21155  mhpmulcl  21249  coe1fsupp  21295  coe1ae0  21297  coe1mul2  21350  coe1tmmul  21358  pmatcoe1fsupp  21758  chfacffsupp  21913  chfacfscmulfsupp  21916  chfacfscmulgsum  21917  chfacfpmmulfsupp  21920  chfacfpmmulgsum  21921  ordtbas2  22250  ordtopn2  22254  ordtrest2lem  22262  pnfnei  22279  ordtt1  22438  ordthauslem  22442  2ndci  22507  2ndcsb  22508  2ndcredom  22509  2ndc1stc  22510  1stcrest  22512  2ndcctbss  22514  2ndcdisj  22515  2ndcsep  22518  lly1stc  22555  tx1stc  22709  ordthmeolem  22860  ufildom1  22985  xmetrtri2  23417  prdsxmetlem  23429  ssblex  23489  prdsbl  23553  comet  23575  stdbdxmet  23577  stdbdmopn  23580  met1stc  23583  dscmet  23634  metdstri  23920  metdscn  23925  xrhmeo  24015  bndth  24027  evth  24028  lebnumlem3  24032  pcovalg  24081  pco1  24084  pcocn  24086  pcopt  24091  pcopt2  24092  pcoass  24093  nmoleub3  24188  bcthlem5  24397  rrxfsupp  24471  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  pmltpclem1  24517  pmltpc  24519  ovollb2lem  24557  ovolctb  24559  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun2  24575  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem3  24588  voliunlem2  24620  voliunlem3  24621  ioombl1lem4  24630  uniioovol  24648  uniioombllem2  24652  uniioombllem3  24654  uniioombllem6  24657  volsup2  24674  ismbfd  24708  mbfsup  24733  mbflimsup  24735  itg1climres  24784  mbfi1fseqlem4  24788  itg2lr  24800  itg2leub  24804  itg2seq  24812  itg2monolem1  24820  itg2monolem3  24822  itg2mono  24823  itg2i1fseq2  24826  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  itg2cn  24833  iblss  24874  itgless  24886  ibladdlem  24889  iblabsr  24899  iblmulc2  24900  itgabs  24904  bddiblnc  24911  ditgeq1  24917  dvferm2lem  25055  rolle  25059  dvlip2  25064  c1liplem1  25065  c1lip1  25066  dvfsumlem2  25096  dvfsumlem4  25098  mdegleb  25134  degltlem1  25142  plyco0  25258  plyeq0lem  25276  coeeq2  25308  dgrle  25309  dgradd2  25334  plydiveu  25363  aareccl  25391  aalioulem2  25398  aaliou3lem7  25414  psercnlem1  25489  pilem2  25516  pilem3  25517  logltb  25660  divlogrlim  25695  logcnlem3  25704  cxpaddlelem  25809  rlimcnp  26020  cxplim  26026  cxploglim  26032  scvxcvx  26040  ftalem1  26127  ftalem2  26128  isppw2  26169  vmappw  26170  sgmnncl  26201  sqff1o  26236  fsumdvdsdiaglem  26237  dvdsppwf1o  26240  dvdsflsumcom  26242  musum  26245  muinv  26247  dvdsmulf1o  26248  vmalelog  26258  vmasum  26269  logfac2  26270  perfectlem2  26283  bcmono  26330  bpos1lem  26335  bposlem9  26345  lgsmod  26376  lgsne0  26388  gausslemma2dlem4  26422  2sqlem6  26476  2sqlem8  26479  2sqlem10  26481  2sqreulem1  26499  2sqreunnlem1  26502  chtppilim  26528  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem2  26543  dchrvmasumlem1  26548  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0  26573  rplogsum  26580  logsqvma  26595  pntpbnd1  26639  pntpbnd2  26640  pntibndlem3  26645  pntlemj  26656  pntlemi  26657  pntlem3  26662  pnt3  26665  ostth3  26691  tgjustc1  26740  tgjustc2  26741  iscgrglt  26779  tgcgr4  26796  hlcgreu  26883  lmif  27050  islmib  27052  trgcopyeu  27071  iscgrad  27076  inaghl  27110  axlowdim2  27231  axlowdim  27232  axcontlem2  27236  axcontlem3  27237  axcontlem4  27238  axcontlem7  27241  axcontlem9  27243  axcontlem10  27244  axcontlem11  27245  axcontlem12  27246  ebtwntg  27253  umgrupgr  27376  nbusgrvtxm1  27649  crctcshwlkn0lem2  28077  crctcshwlkn0lem3  28078  crctcsh  28090  wlkswwlksf1o  28145  clwlkclwwlklem2fv1  28260  clwlkclwwlkf  28273  0clwlkv  28396  eupth2  28504  numclwwlk5  28653  nmoubi  29035  minvecolem2  29138  minvecolem3  29139  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  htthlem  29180  chlimi  29497  chcompl  29505  hsn0elch  29511  cmbr3  29871  cmcm  29877  cmcm3  29878  lecm  29880  nmopub  30171  nmfnleub  30188  nmopun  30277  nmcexi  30289  cnlnadjlem7  30336  pjnmopi  30411  stle0i  30502  stlesi  30504  stm1i  30506  csmdsymi  30597  cvmd  30599  atcveq0  30611  atcv1  30643  atord  30651  atcvat2  30652  chirred  30658  mdsym  30675  mddmdin0i  30694  cdj1i  30696  fmptcof2  30896  fnpreimac  30910  isoun  30936  fcobijfs  30960  lt2addrd  30976  xlt2addrd  30983  xrge0infss  30985  infxrge0glb  30990  xrofsup  30992  fz1nnct  31026  toslublem  31152  tosglblem  31154  ismntd  31164  mgccole1  31170  mgccole2  31171  mgcmnt1  31172  mgcmnt2  31173  dfmgc2lem  31175  dfmgc2  31176  omndadd  31234  psgnfzto1stlem  31269  fzto1st  31272  psgnfzto1st  31274  trsp2cyc  31292  xrnarchi  31340  archirng  31344  archiexdiv  31346  archiabl  31354  isarchiofld  31418  linds2eq  31477  elrspunidl  31508  isrprm  31567  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  smatrcl  31648  smatlem  31649  madjusmdetlem2  31680  madjusmdet  31683  cmpcref  31702  ldlfcntref  31706  dispcmp  31711  zarcmplem  31733  ordtrest2NEWlem  31774  ordtconnlem1  31776  xrge0iifiso  31787  rge0scvg  31801  gsumesum  31927  esumfsup  31938  esumpinfval  31941  esumpcvgval  31946  esumcvg  31954  sigaclcu  31985  sigaclci  32000  unelsiga  32002  unelldsys  32026  sigapildsys  32030  ldgenpisyslem1  32031  fiunelros  32042  measvun  32077  voliune  32097  volfiniune  32098  oms0  32164  omssubaddlem  32166  omssubadd  32167  carsgsigalem  32182  carsgclctunlem2  32186  carsgclctun  32188  pmeasmono  32191  pmeasadd  32192  orvcval2  32325  dstfrvel  32340  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemsv  32376  ballotlemsf1o  32380  sgnmulsgn  32416  breprexp  32513  tgoldbachgt  32543  bnj23  32597  bnj1185  32673  bnj1152  32878  bnj1418  32920  fnrelpredd  32961  loop1cycl  32999  umgr2cycl  33003  acycgrcycl  33009  eqfunresadj  33641  dfdm5  33653  dfrn5  33654  ttrclss  33706  poxp2  33717  frxp2  33718  poxp3  33723  frxp3  33724  xpord3pred  33725  poseq  33729  wzel  33745  wsuclem  33746  nodense  33822  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupdm  33834  nosupbnd1lem1  33838  nosupbnd1lem4  33841  nosupbnd1  33844  nosupbnd2lem1  33845  nosupbnd2  33846  noinfcbv  33847  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noinfbnd1  33859  noetalem2  33872  nocvxminlem  33899  ssltsepc  33914  conway  33920  scutval  33921  etasslt  33934  slerec  33940  bday1s  33952  madeval2  33964  rightval  33975  ssltright  33982  made0  33984  madecut  33992  madebdaylemlrcut  34006  sltlpss  34014  cofsslt  34015  coinitsslt  34016  cofcutr  34019  cofcutrtime  34020  brpprod  34114  brsset  34118  brbigcup  34127  dffix2  34134  elfuns  34144  brimageg  34156  brdomaing  34164  brrangeg  34165  brimg  34166  brapply  34167  brsuccf  34170  funpartlem  34171  brrestrict  34178  dfrecs2  34179  dfrdg4  34180  brofs  34234  btwncomim  34242  btwnintr  34248  btwnexch3  34249  btwnexch2  34252  brifs  34272  brcolinear2  34287  colineardim1  34290  brfs  34308  btwnconn1  34330  segcon2  34334  seglerflx  34341  seglemin  34342  btwnsegle  34346  colinbtwnle  34347  broutsideof2  34351  fvray  34370  lineunray  34376  lineelsb2  34377  linerflx1  34378  trer  34432  elicc3  34433  finminlem  34434  nn0prpwlem  34438  nn0prpw  34439  fnessref  34473  refssfne  34474  unblimceq0lem  34613  unblimceq0  34614  unbdqndv2  34618  knoppndvlem21  34639  taupilemrplb  35418  dfgcd3  35422  icorempo  35449  icoreval  35451  iooelexlt  35460  relowlssretop  35461  domalom  35502  ctbssinf  35504  pibt2  35515  phpreu  35688  fin2solem  35690  fin2so  35691  ltflcei  35692  ptrecube  35704  poimirlem1  35705  poimirlem2  35706  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem12  35716  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem32  35736  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ibladdnclem  35760  iblmulc2nc  35769  itgabsnc  35773  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  indexdom  35819  filbcmb  35825  fdc  35830  prdsbnd  35878  heiborlem3  35898  rrnequiv  35920  rngoueqz  36025  inxprnres  36354  eqvreltr  36647  prtlem10  36806  lsatcveq0  36973  lsatcv1  36989  oposlem  37123  opnlen0  37129  lub0N  37130  glb0N  37134  omllaw  37184  cmtbr4N  37196  cvrval  37210  cvrnbtwn  37212  cvrnbtwn2  37216  cvrnbtwn3  37217  cvrcon3b  37218  cvrnbtwn4  37220  atcvreq0  37255  atnle  37258  atlatmstc  37260  cvlexch1  37269  glbconN  37318  hlsuprexch  37322  exatleN  37345  cvratlem  37362  atcvrj0  37369  atcvrj2b  37373  atlelt  37379  cvrat4  37384  3dim1lem5  37407  3dim2  37409  3dim3  37410  ps-2  37419  llni  37449  llnn0  37457  llnle  37459  lplni  37473  lplni2  37478  lplnle  37481  lplnn0N  37488  llncvrlpln  37499  2llnjN  37508  lvoli  37516  lvoli3  37518  lvoli2  37522  lvoln0N  37532  4at  37554  lplncvrlvol  37557  2lplnj  37561  dalemcea  37601  dalem3  37605  psubspi  37688  linepsubN  37693  elpmap  37699  pmapsub  37709  lnatexN  37720  cdlema1N  37732  cdlemb  37735  elpadd  37740  paddvaln0N  37742  paddasslem5  37765  llnexchb2lem  37809  llnexch2N  37811  islhp  37937  lhpat3  37987  4atexlemex2  38012  4atex  38017  4atex2-0aOLDN  38019  4atex2-0cOLDN  38021  lautle  38025  lautcvr  38033  lauteq  38036  ldilval  38054  ltrnu  38062  trlval2  38104  trlne  38126  cdleme0ex1N  38164  cdleme0nex  38231  cdleme18d  38236  cdlemednuN  38241  cdleme25b  38295  cdleme25cv  38299  cdleme27b  38309  cdleme29b  38316  cdleme31sn  38321  cdleme31fv  38331  cdleme31fv2  38334  cdlemefrs29bpre0  38337  cdlemefr29bpre0N  38347  cdlemefr29clN  38348  cdlemefr32fvaN  38350  cdlemefr32fva1  38351  cdlemefs29pre00N  38353  cdlemefs32sn1aw  38355  cdlemefs29bpre0N  38357  cdlemefs29bpre1N  38358  cdlemefs29cpre1N  38359  cdlemefs29clN  38360  cdlemefs32fvaN  38363  cdlemefs32fva1  38364  cdleme41sn3a  38374  cdleme32fva  38378  cdleme32e  38386  cdleme35f  38395  cdleme40v  38410  cdleme42b  38419  trlord  38510  cdlemg1cex  38529  diaval  38973  diaeldm  38977  diaelrnN  38986  cdlemm10N  39059  dibglbN  39107  dicval  39117  dicfnN  39124  dicvalrelN  39126  dihval  39173  dihlsscpre  39175  dihglblem3N  39236  dihmeetlem2N  39240  djhcvat42  39356  lcmineqlem4  39968  aks4d1p4  40015  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  sticksstones1  40030  sticksstones2  40031  sticksstones10  40039  sticksstones12a  40041  metakunt3  40055  metakunt4  40056  metakunt6  40058  metakunt7  40059  metakunt8  40060  metakunt10  40062  metakunt11  40063  metakunt12  40064  metakunt20  40072  metakunt21  40073  metakunt22  40074  metakunt30  40082  qsalrel  40141  dvdsexpnn0  40262  sn-sup2  40360  flt4lem2  40400  flt4lem7  40412  lzenom  40508  fphpdo  40555  irrapxlem4  40563  pellexlem6  40572  infmrgelbi  40616  pellfundre  40619  pellfundlb  40622  monotoddzz  40681  zindbi  40684  jm2.27  40746  rmydioph  40752  rpnnen3lem  40769  fnwe2lem2  40792  aomclem8  40802  hbtlem5  40869  hbt  40871  ensucne0  41034  en2pr  41043  pr2cv  41044  refimssco  41104  rfovfvfvd  41500  rfovcnvf1od  41501  fsovrfovd  41506  nzss  41824  wessf1ornlem  42611  axccdom  42651  dmrelrnrel  42654  axccd  42657  rnmptlb  42677  rnmptbdd  42679  rnmptbd2  42684  rnmptbdlem  42690  rnmptbd  42691  dstregt0  42709  suplesup  42768  supxrunb3  42829  supxrleubrnmpt  42836  rexabslelem  42848  rexabsle  42849  suprleubrnmpt  42852  infrnmptle  42853  infxrunb3rnmpt  42858  infxrpnf  42876  supminfxr  42894  infrpgernmpt  42895  xrpnf  42916  limsupre  43072  limsupref  43116  limsupbnd1f  43117  limsuppnfd  43133  climinf2  43138  limsuppnf  43142  climinfmpt  43146  climinf3  43147  limsupmnflem  43151  limsupmnf  43152  limsupre2  43156  limsupmnfuzlem  43157  limsupre2mpt  43161  limsupre3lem  43163  limsupre3  43164  limsupre3mpt  43165  limsupre3uzlem  43166  limsupre3uz  43167  limsupreuz  43168  limsupreuzmpt  43170  liminfval2  43199  liminfreuzlem  43233  liminfreuz  43234  xlimpnfxnegmnf  43245  cnrefiisplem  43260  xlimpnfv  43269  xlimpnf  43273  xlimpnfmpt  43275  dfxlim2  43279  icccncfext  43318  cncficcgt0  43319  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem5  43436  stoweidlem20  43451  stoweidlem26  43457  stoweidlem28  43459  stoweidlem29  43460  stoweidlem34  43465  wallispilem3  43498  stirlinglem13  43517  fourierdlem41  43579  fourierdlem42  43580  fourierdlem51  43588  fourierdlem54  43591  salunicl  43747  saluncl  43748  salexct  43763  salexct2  43768  salexct3  43771  salgencntex  43772  salgensscntex  43773  sge0pnffigt  43824  meadjuni  43885  omeunile  43933  ovnlerp  43990  hoidifhspval  44036  ovolval5lem2  44081  salpreimagelt  44132  pimincfltioo  44142  salpreimagtge  44148  salpreimagtlt  44153  incsmf  44165  issmfgt  44179  smfpreimagt  44184  decsmf  44189  issmfge  44192  smfpimgtxr  44202  smfpreimage  44204  smfinflem  44237  smfinf  44238  funressnfv  44424  funressnvmo  44426  funressnmo  44427  dfdfat2  44507  tz6.12-afv  44552  funressndmafv2rn  44602  tz6.12-afv2  44619  dfatcolem  44634  dfatco  44635  iccpartigtl  44763  iccpartgt  44767  icceuelpartlem  44775  iccpartnel  44778  sprsymrelfolem2  44833  goldbachthlem2  44886  odz2prm2pw  44903  fmtnoprmfac1  44905  fmtnoprmfac2  44907  fmtnofac2  44909  fmtno4prmfac  44912  fmtno4prm  44915  prmdvdsfmtnof1lem1  44924  31prm  44937  perfectALTVlem2  45062  nnsum3primes4  45128  nnsum3primesprm  45130  nnsum3primesgbe  45132  nnsum3primesle9  45134  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgblthelfgott  45155  tgoldbach  45157  assintop  45291  isassintop  45292  assintopcllaw  45294  ztprmneprm  45571  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  lco0  45656  lcoel0  45657  lincsumcl  45660  lincscmcl  45661  lcoss  45665  linindslinci  45677  lindslinindsimp1  45686  linds0  45694  el0ldep  45695  lindsrng01  45697  ldepspr  45702  islindeps2  45712  isldepslvec2  45714  zlmodzxzldep  45733  ldepsnlinc  45737  elbigo2r  45787  lubsscl  46142  glbsscl  46143  lubprlem  46144  ipolub  46162  ipoglb  46165  catprslem  46179  setrec2lem1  46285