Theorem breq1 4656

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  ⟨cop 4183   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breq12  4658  breq1i  4660  breq1d  4663  nbrne2  4673  brab1  4700  pocl  5042  swopolem  5044  swopo  5045  solin  5058  sotrieq  5062  sotr2  5064  isso2i  5067  somo  5069  frirr  5091  fr2nr  5092  wereu2  5111  vtoclr  5164  frsn  5189  brcog  5288  brcogw  5290  opelcnvg  5302  dfdmf  5317  eldmg  5319  dfrnf  5364  dfres2  5453  imasng  5487  asymref2  5513  sotri2  5525  somin1  5529  coi1  5651  dffun6f  5902  funmo  5904  fun11  5963  fveq2  6191  eliman0  6223  nfunsn  6225  dffv2  6271  fvopab5  6309  dff3  6372  f1ompt  6382  fmptco  6396  dff13  6512  foeqcnvco  6555  isorel  6576  soisores  6577  soisoi  6578  isocnv  6580  isotr  6586  isomin  6587  isoini  6588  isopolem  6595  isosolem  6597  f1oiso  6601  f1oiso2  6602  weniso  6604  caovordig  6839  caovordg  6841  caovord3d  6844  caovord  6845  caovord3  6847  caofrss  6930  caoftrn  6932  fr3nr  6979  dfwe2  6981  f1oweALT  7152  frxp  7287  poxp  7289  fnse  7294  brtpos2  7358  rntpos  7365  tpostpos  7372  ertr  7757  ecopovsym  7849  ecopovtrn  7850  isfi  7979  en0  8019  en1  8023  endisj  8047  xpcomco  8050  sbth  8080  2pwne  8116  disjenex  8118  ssenen  8134  nneneq  8143  php  8144  sdom1  8160  isinf  8173  fineqvlem  8174  pssnn  8178  en1eqsnbi  8191  enp1i  8195  findcard  8199  findcard2  8200  findcard3  8203  frfi  8205  fiint  8237  mapfienlem1  8310  mapfienlem2  8311  mapfienlem3  8312  mapfien  8313  marypha1lem  8339  supmo  8358  eqsup  8362  supub  8365  suplub  8366  suppr  8377  supisolem  8379  supisoex  8380  infmin  8400  infmo  8401  fiinfg  8405  fiinf2g  8406  infpr  8409  ordtypecbv  8422  ordtypelem3  8425  ordtypelem6  8428  ordtypelem7  8429  ordtypelem9  8431  ordtypelem10  8432  hartogslem1  8447  hartogs  8449  wemaplem1  8451  wemaplem2  8452  wemapso2lem  8457  card2on  8459  card2inf  8460  elharval  8468  brwdom2  8478  wdomtr  8480  cantnfs  8563  cantnfp1lem2  8576  oemapso  8579  cantnflem1  8586  wemapwe  8594  r111  8638  kardex  8757  karden  8758  isnumi  8772  tskwe  8776  cardid2  8779  cardonle  8783  cardne  8791  iscard2  8802  infxpenlem  8836  fodomfi2  8883  wdomfil  8884  wdomnumr  8887  alephsuc2  8903  infenaleph  8914  iunfictbso  8937  infpss  9039  cff1  9080  cfslb2n  9090  sornom  9099  fin4i  9120  isfin6  9122  isfin7  9123  isfin1-3  9208  fin1a2lem9  9230  fin1a2lem11  9232  hsmexlem4  9251  axcc2lem  9258  axcc4dom  9263  domtriomlem  9264  numthcor  9316  zorn2lem2  9319  zorn2lem3  9320  zorn2lem7  9324  zorn2g  9325  axdclem  9341  axdc  9343  brdom7disj  9353  brdom6disj  9354  uniimadom  9366  ondomon  9385  alephval2  9394  alephreg  9404  pwcfsdom  9405  elgch  9444  gchi  9446  fpwwe2lem12  9463  fpwwe2lem13  9464  pwfseqlem4  9484  winainflem  9515  winalim2  9518  tsken  9576  0tsk  9577  inar1  9597  tskord  9602  tskuni  9605  grudomon  9639  pinq  9749  nqereu  9751  enqeq  9756  ltbtwnnq  9800  ltrnq  9801  prcdnq  9815  prnmax  9817  genpnmax  9829  nqpr  9836  1idpr  9851  reclem2pr  9870  reclem3pr  9871  reclem4pr  9872  recexpr  9873  supexpr  9876  ltsosr  9915  1ne0sr  9917  ltasr  9921  supsrlem  9932  axpre-lttri  9986  axpre-lttrn  9987  axpre-ltadd  9988  axpre-sup  9990  lelttr  10128  dedekind  10200  dedekindle  10201  ltordlem  10553  lt0ne0d  10593  fimaxre3  10970  fiminre  10972  lbreu  10973  lble  10975  sup2  10979  infm3  10982  suprleub  10989  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmul  10995  nnsub  11059  nominpos  11269  nnunb  11288  arch  11289  nn0sub  11343  nn0n0n1ge2b  11359  nn0lt10b  11439  zextle  11450  peano5uzti  11467  fzind  11475  btwnz  11479  uzval  11689  uzwo  11751  nnwof  11754  ublbneg  11773  lbzbi  11776  zsupss  11777  uzsupss  11780  uzwo3  11783  zmax  11785  rebtwnz  11787  rpnnen1lem3  11816  rpnnen1lem3OLD  11822  xrltnsym  11970  xrlttri  11972  xrlttr  11973  xrlelttr  11987  nltpnft  11995  xrmaxlt  12012  xrmaxle  12014  qbtwnre  12030  qbtwnxr  12031  xltnegi  12047  xnn0lenn0nn0  12075  xsubge0  12091  xlesubadd  12093  xmullem2  12095  xlemul1a  12118  xrinfmexpnf  12136  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrunb1  12149  supxrunb2  12150  reltre  12170  rpltrp  12171  reltxrnmnf  12172  ixxval  12183  elixx1  12184  elioo2  12216  iccid  12220  icc0  12223  fzval  12328  elfz1  12331  elfznelfzo  12573  elfznelfzob  12574  flval  12595  fllelt  12598  flflp1  12608  flval2  12615  flval3  12616  flbi  12617  dfceil2  12640  ceilval2  12641  fleqceilz  12653  modid2  12697  addmodlteq  12745  fsequb2  12775  ssnn0fi  12784  seqf1olem2  12841  sqlecan  12971  faclbnd4lem1  13080  hashsnle1  13205  pr2pwpr  13261  swrdccatid  13497  rtrclreclem3  13800  relexpindlem  13803  sgnval  13828  sqrlem6  13988  01sqrex  13990  abslt  14054  absle  14055  rexanre  14086  rexico  14093  limsupgle  14208  limsupgre  14212  limsupbnd2  14214  rlim2lt  14228  rlim3  14229  ello12r  14248  ello1d  14254  elo12r  14259  rlimconst  14275  climshft  14307  rlimcn2  14321  o1rlimmul  14349  lo1le  14382  climsup  14400  caucvgrlem  14403  isumless  14577  divrcnv  14584  cvgrat  14615  rpnnen2lem10  14952  ruclem1  14960  ruclem2  14961  ruclem11  14969  ruclem12  14970  sqrt2irr  14979  absdvdsb  15000  dvdsle  15032  dvdsabseq  15035  dvdsdivcl  15038  dvdsext  15043  divalglem8  15123  divalglem9  15124  divalglem10  15125  divalgmod  15129  divalgmodOLD  15130  ndvdssub  15133  sadcaddlem  15179  gcdcllem1  15221  gcdcllem2  15222  gcdcllem3  15223  dfgcd2  15263  gcdzeq  15271  dvdssq  15280  nn0seqcvgd  15283  algcvgblem  15290  lcmval  15305  lcmdvds  15321  lcmgcdeq  15325  lcmfpr  15340  lcmf  15346  lcmftp  15349  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfdvdsb  15356  coprmgcdb  15362  coprmdvds1  15365  1nprm  15392  1idssfct  15393  isprm2lem  15394  isprm2  15395  dvdsprime  15400  nprm  15401  3prm  15406  dvdsprm  15415  exprmfct  15416  isprm5  15419  maxprmfct  15421  coprm  15423  ncoprmlnprm  15436  eulerthlem2  15487  phisum  15495  odzval  15496  pythagtriplem4  15524  pc2dvds  15583  pcprmpw2  15586  pcprmpw  15587  dvdsprmpweqle  15590  oddprmdvds  15607  prmpwdvds  15608  pockthg  15610  unbenlem  15612  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  1arith  15631  vdwlem6  15690  vdwlem11  15695  vdwlem13  15697  ramtlecl  15704  ramub  15717  rami  15719  ramubcl  15722  0ram  15724  ram0  15726  prmdvdsprmop  15747  prmolefac  15750  prmodvdslcmf  15751  prmgaplem2  15754  prmgaplcmlem1  15755  prmgaplcmlem2  15756  prmgaplem3  15757  prmgaplem4  15758  prmgaplem5  15759  prmgaplem6  15760  prmgapprmolem  15765  prmlem0  15812  prmlem1a  15813  imasaddfnlem  16188  imasvscafn  16197  imasleval  16201  prslem  16931  drsdir  16935  drsdirfi  16938  isdrs2  16939  posi  16950  posasymb  16952  pltval3  16967  plelttr  16972  pospo  16973  lubprop  16986  luble  16987  lublecllem  16988  glbprop  16999  joinval2lem  17008  joinlem  17011  meetlem  17025  meetle  17028  latnlej  17068  isglbd  17117  lubub  17119  lubun  17123  clatleglb  17126  pospropd  17134  poslubmo  17146  posglbmo  17147  poslubd  17148  tsrlin  17219  letsr  17227  dirge  17237  pmtrval  17871  pmtrrn  17877  pmtrfrn  17878  pmtrrn2  17880  pmtrsn  17939  mndodcongi  17962  odeq  17969  odmulgeq  17974  gexnnod  18003  sylow1lem1  18013  pgpssslw  18029  sylow2a  18034  efgredeu  18165  efgred2  18166  gexex  18256  frgpnabllem2  18277  cyggenod  18286  dprdval  18402  dprdw  18409  dprdwd  18410  ablfacrplem  18464  ablfac1c  18470  ablfac1eu  18472  ablfaclem3  18486  abvtrivd  18840  psrbagconcl  19373  psrbagconf1o  19374  gsumbagdiaglem  19375  psrmulcllem  19387  psrlidm  19403  psrridm  19404  psrass1  19405  psrcom  19409  mplelbas  19430  mplmonmul  19464  ltbwe  19472  coe1fsupp  19584  coe1ae0  19586  coe1mul2  19639  coe1tmmul  19647  zringlpir  19837  prmirredlem  19841  znleval  19903  frlmelbas  20100  ellspd  20141  islindf4  20177  pmatcoe1fsupp  20506  chfacffsupp  20661  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  ordtbas2  20995  ordtopn2  20999  ordtrest2lem  21007  pnfnei  21024  ordtt1  21183  ordthauslem  21187  2ndci  21251  2ndcsb  21252  2ndcredom  21253  2ndc1stc  21254  1stcrest  21256  2ndcctbss  21258  2ndcdisj  21259  2ndcsep  21262  lly1stc  21299  tx1stc  21453  ordthmeolem  21604  ufildom1  21730  xmetrtri2  22161  prdsxmetlem  22173  ssblex  22233  prdsbl  22296  comet  22318  stdbdxmet  22320  stdbdmopn  22323  met1stc  22326  dscmet  22377  metdstri  22654  metdscn  22659  xrhmeo  22745  bndth  22757  evth  22758  lebnumlem3  22762  pcovalg  22812  pco1  22815  pcocn  22817  pcopt  22822  pcopt2  22823  pcoass  22824  nmoleub3  22919  bcthlem5  23125  rrxfsupp  23185  minveclem4c  23196  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  pmltpclem1  23217  pmltpc  23219  ovollb2lem  23256  ovolctb  23258  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun2  23274  ovolshftlem1  23277  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem3  23287  voliunlem2  23319  voliunlem3  23320  ioombl1lem4  23329  uniioovol  23347  uniioombllem2  23351  uniioombllem3  23353  uniioombllem6  23356  volsup2  23373  ismbfd  23407  mbfsup  23431  mbflimsup  23433  itg1climres  23481  mbfi1fseqlem4  23485  itg2lr  23497  itg2leub  23501  itg2seq  23509  itg2monolem1  23517  itg2monolem3  23519  itg2mono  23520  itg2i1fseq2  23523  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  itg2cn  23530  iblss  23571  itgless  23583  ibladdlem  23586  iblabsr  23596  iblmulc2  23597  itgabs  23601  ditgeq1  23612  dvferm2lem  23749  rolle  23753  dvlip2  23758  c1liplem1  23759  c1lip1  23760  dvfsumlem2  23790  dvfsumlem4  23792  mdegleb  23824  degltlem1  23832  plyco0  23948  plyeq0lem  23966  coeeq2  23998  dgrle  23999  dgradd2  24024  plydiveu  24053  aareccl  24081  aalioulem2  24088  aaliou3lem7  24104  psercnlem1  24179  pilem2  24206  pilem3  24207  logltb  24346  divlogrlim  24381  logcnlem3  24390  cxpaddlelem  24492  rlimcnp  24692  cxplim  24698  cxploglim  24704  scvxcvx  24712  ftalem1  24799  ftalem2  24800  isppw2  24841  vmappw  24842  sgmnncl  24873  sqff1o  24908  fsumdvdsdiaglem  24909  dvdsppwf1o  24912  dvdsflsumcom  24914  musum  24917  muinv  24919  dvdsmulf1o  24920  vmalelog  24930  vmasum  24941  logfac2  24942  perfectlem2  24955  bcmono  25002  bpos1lem  25007  bposlem9  25017  lgsmod  25048  lgsne0  25060  gausslemma2dlem4  25094  2sqlem6  25148  2sqlem8  25151  2sqlem10  25153  chtppilim  25164  rpvmasumlem  25176  dchrisumlema  25177  dchrisumlem2  25179  dchrvmasumlem1  25184  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0  25209  rplogsum  25216  logsqvma  25231  pntpbnd1  25275  pntpbnd2  25276  pntibndlem3  25281  pntlemj  25292  pntlemi  25293  pntlem3  25298  pnt3  25301  ostth3  25327  iscgrglt  25409  tgcgr4  25426  hlcgreu  25513  lmif  25677  islmib  25679  trgcopyeu  25698  iscgrad  25703  inaghl  25731  axlowdim2  25840  axlowdim  25841  axcontlem2  25845  axcontlem3  25846  axcontlem4  25847  axcontlem7  25850  axcontlem9  25852  axcontlem10  25853  axcontlem11  25854  axcontlem12  25855  ebtwntg  25862  umgrupgr  25998  nbusgrvtxm1  26281  crctcshwlkn0lem2  26703  crctcshwlkn0lem3  26704  crctcsh  26716  wlkpwwlkf1ouspgr  26765  clwlkclwwlklem2fv1  26896  clwlksf1clwwlklem1  26965  eupth2  27099  numclwwlk5  27246  nmoubi  27627  minvecolem2  27731  minvecolem3  27732  minvecolem4c  27735  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  htthlem  27774  chlimi  28091  chcompl  28099  hsn0elch  28105  cmbr3  28467  cmcm  28473  cmcm3  28474  lecm  28476  nmopub  28767  nmfnleub  28784  nmopun  28873  nmcexi  28885  cnlnadjlem7  28932  pjnmopi  29007  stle0i  29098  stlesi  29100  stm1i  29102  csmdsymi  29193  cvmd  29195  atcveq0  29207  atcv1  29239  atord  29247  atcvat2  29248  chirred  29254  mdsym  29271  mddmdin0i  29290  cdj1i  29292  fmptcof2  29457  isoun  29479  fcobijfs  29501  lt2addrd  29516  xlt2addrd  29523  xrge0infss  29525  infxrge0glb  29530  xrofsup  29533  fz1nnct  29560  tleile  29661  toslublem  29667  tosglblem  29669  omndadd  29706  xrnarchi  29738  archirng  29742  archiexdiv  29744  archiabl  29752  isarchiofld  29817  psgnfzto1stlem  29850  fzto1st  29853  psgnfzto1st  29855  smatrcl  29862  smatlem  29863  madjusmdetlem2  29894  madjusmdet  29897  cmpcref  29917  ldlfcntref  29921  dispcmp  29926  ordtrest2NEWlem  29968  ordtconnlem1  29970  xrge0iifiso  29981  rge0scvg  29995  gsumesum  30121  esumfsup  30132  esumpinfval  30135  esumpcvgval  30140  esumcvg  30148  sigaclcu  30180  sigaclci  30195  unelsiga  30197  unelldsys  30221  sigapildsys  30225  ldgenpisyslem1  30226  fiunelros  30237  measvun  30272  voliune  30292  volfiniune  30293  oms0  30359  omssubaddlem  30361  omssubadd  30362  carsgsigalem  30377  carsgclctunlem2  30381  carsgclctun  30383  pmeasmono  30386  pmeasadd  30387  orvcval2  30520  dstfrvel  30535  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsv  30571  ballotlemsf1o  30575  sgnmulsgn  30611  breprexp  30711  tgoldbachgt  30741  bnj23  30784  bnj1185  30864  bnj1152  31066  bnj1418  31108  eqfunresadj  31659  dfdm5  31676  dfrn5  31677  trpredpred  31728  poseq  31750  wzel  31771  wsuclem  31773  wsuclemOLD  31774  nodense  31842  noresle  31846  noprefixmo  31848  nosupdm  31850  nosupbnd1lem1  31854  nosupbnd1lem4  31857  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  noetalem5  31867  nocvxminlem  31893  conway  31910  scutval  31911  etasslt  31920  slerec  31923  madeval2  31936  brpprod  31992  brsset  31996  brbigcup  32005  dffix2  32012  elfuns  32022  brimageg  32034  brdomaing  32042  brrangeg  32043  brimg  32044  brapply  32045  brsuccf  32048  funpartlem  32049  brrestrict  32056  dfrecs2  32057  dfrdg4  32058  brofs  32112  btwncomim  32120  btwnintr  32126  btwnexch3  32127  btwnexch2  32130  brifs  32150  brcolinear2  32165  colineardim1  32168  brfs  32186  btwnconn1  32208  segcon2  32212  seglerflx  32219  seglemin  32220  btwnsegle  32224  colinbtwnle  32225  broutsideof2  32229  fvray  32248  lineunray  32254  lineelsb2  32255  linerflx1  32256  trer  32310  elicc3  32311  finminlem  32312  nn0prpwlem  32317  nn0prpw  32318  fnessref  32352  refssfne  32353  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2  32502  knoppndvlem21  32523  taupilemrplb  33166  dfgcd3  33170  icorempt2  33199  icoreval  33201  iooelexlt  33210  relowlssretop  33211  phpreu  33393  fin2solem  33395  fin2so  33396  ltflcei  33397  ptrecube  33409  poimirlem1  33410  poimirlem2  33411  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem12  33421  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  poimirlem32  33441  heicant  33444  mblfinlem1  33446  mblfinlem2  33447  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  iblmulc2nc  33475  itgabsnc  33479  bddiblnc  33480  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  indexdom  33529  filbcmb  33535  fdc  33541  prdsbnd  33592  heiborlem3  33612  rrnequiv  33634  rngoueqz  33739  inxprnres  34060  prtlem10  34150  lsatcveq0  34319  lsatcv1  34335  oposlem  34469  opnlen0  34475  lub0N  34476  glb0N  34480  omllaw  34530  cmtbr4N  34542  cvrval  34556  cvrnbtwn  34558  cvrnbtwn2  34562  cvrnbtwn3  34563  cvrcon3b  34564  cvrnbtwn4  34566  atcvreq0  34601  atnle  34604  atlatmstc  34606  cvlexch1  34615  glbconN  34663  hlsuprexch  34667  exatleN  34690  cvratlem  34707  atcvrj0  34714  atcvrj2b  34718  atlelt  34724  cvrat4  34729  3dim1lem5  34752  3dim2  34754  3dim3  34755  ps-2  34764  llni  34794  llnn0  34802  llnle  34804  lplni  34818  lplni2  34823  lplnle  34826  lplnn0N  34833  llncvrlpln  34844  2llnjN  34853  lvoli  34861  lvoli3  34863  lvoli2  34867  lvoln0N  34877  4at  34899  lplncvrlvol  34902  2lplnj  34906  dalemcea  34946  dalem3  34950  psubspi  35033  linepsubN  35038  elpmap  35044  pmapsub  35054  lnatexN  35065  cdlema1N  35077  cdlemb  35080  elpadd  35085  paddvaln0N  35087  paddasslem5  35110  llnexchb2lem  35154  llnexch2N  35156  islhp  35282  lhpat3  35332  4atexlemex2  35357  4atex  35362  4atex2-0aOLDN  35364  4atex2-0cOLDN  35366  lautle  35370  lautcvr  35378  lauteq  35381  ldilval  35399  ltrnu  35407  trlval2  35450  trlne  35472  cdleme0ex1N  35510  cdleme0nex  35577  cdleme18d  35582  cdlemednuN  35587  cdleme25b  35642  cdleme25cv  35646  cdleme27b  35656  cdleme29b  35663  cdleme31sn  35668  cdleme31fv  35678  cdleme31fv2  35681  cdlemefrs29bpre0  35684  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdlemefs29pre00N  35700  cdlemefs32sn1aw  35702  cdlemefs29bpre0N  35704  cdlemefs29bpre1N  35705  cdlemefs29cpre1N  35706  cdlemefs29clN  35707  cdlemefs32fvaN  35710  cdlemefs32fva1  35711  cdleme41sn3a  35721  cdleme32fva  35725  cdleme32e  35733  cdleme35f  35742  cdleme40v  35757  cdleme42b  35766  trlord  35857  cdlemg1cex  35876  diaval  36321  diaeldm  36325  diaelrnN  36334  cdlemm10N  36407  dibglbN  36455  dicval  36465  dicfnN  36472  dicvalrelN  36474  dihval  36521  dihlsscpre  36523  dihglblem3N  36584  dihmeetlem2N  36588  djhcvat42  36704  lzenom  37333  fphpdo  37381  irrapxlem4  37389  pellexlem6  37398  infmrgelbi  37442  pellfundre  37445  pellfundlb  37448  monotoddzz  37508  zindbi  37511  jm2.27  37575  rmydioph  37581  rpnnen3lem  37598  fnwe2lem2  37621  aomclem8  37631  hbtlem5  37698  hbt  37700  refimssco  37913  rfovfvfvd  38297  rfovcnvf1od  38298  fsovrfovd  38303  nzss  38516  wessf1ornlem  39371  axccdom  39416  dmrelrnrel  39419  axccd  39429  rnmptlb  39453  rnmptbdd  39456  rnmptbd2  39464  rnmptbdlem  39470  rnmptbd  39471  dstregt0  39493  suplesup  39555  fiminre2  39594  supxrunb3  39623  supxrleubrnmpt  39632  rexabslelem  39645  rexabsle  39646  suprleubrnmpt  39649  infrnmptle  39650  infxrunb3rnmpt  39655  infxrpnf  39674  supminfxr  39694  infrpgernmpt  39695  limsupre  39873  limsupref  39917  limsupbnd1f  39918  limsuppnfd  39934  climinf2  39939  limsuppnf  39943  climinfmpt  39947  climinf3  39948  limsupmnflem  39952  limsupmnf  39953  limsupre2  39957  limsupmnfuzlem  39958  limsupre2mpt  39962  limsupre3lem  39964  limsupre3  39965  limsupre3mpt  39966  limsupre3uzlem  39967  limsupre3uz  39968  limsupreuz  39969  limsupreuzmpt  39971  liminfval2  40000  liminfreuzlem  40034  liminfreuz  40035  cnrefiisplem  40055  xlimpnfv  40064  xlimpnf  40068  xlimpnfmpt  40070  dfxlim2  40074  icccncfext  40100  cncficcgt0  40101  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem5  40222  stoweidlem20  40237  stoweidlem26  40243  stoweidlem28  40245  stoweidlem29  40246  stoweidlem34  40251  wallispilem3  40284  stirlinglem13  40303  fourierdlem41  40365  fourierdlem42  40366  fourierdlem51  40374  fourierdlem54  40377  salunicl  40536  saluncl  40537  salexct  40552  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  sge0pnffigt  40613  meadjuni  40674  omeunile  40719  ovnlerp  40776  hoidifhspval  40822  ovolval5lem2  40867  salpreimagelt  40918  pimincfltioo  40928  salpreimagtge  40934  salpreimagtlt  40939  incsmf  40951  issmfgt  40965  smfpreimagt  40970  decsmf  40975  issmfge  40978  smfpimgtxr  40988  smfpreimage  40990  smfinflem  41023  smfinf  41024  funressnfv  41208  dfdfat2  41211  tz6.12-afv  41253  iccpartigtl  41359  iccpartgt  41363  icceuelpartlem  41371  iccpartnel  41374  goldbachthlem2  41458  odz2prm2pw  41475  fmtnoprmfac1  41477  fmtnoprmfac2  41479  fmtnofac2  41481  fmtno4prmfac  41484  fmtno4prm  41487  prmdvdsfmtnof1lem1  41496  31prm  41512  perfectALTVlem2  41631  nnsum3primes4  41676  nnsum3primesprm  41678  nnsum3primesgbe  41680  nnsum3primesle9  41682  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgblthelfgott  41703  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  sprsymrelfolem2  41743  assintop  41845  isassintop  41846  assintopcllaw  41848  ztprmneprm  42125  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  lco0  42216  lcoel0  42217  lincsumcl  42220  lincscmcl  42221  lcoss  42225  linindslinci  42237  lindslinindsimp1  42246  linds0  42254  el0ldep  42255  lindsrng01  42257  ldepspr  42262  islindeps2  42272  isldepslvec2  42274  zlmodzxzldep  42293  ldepsnlinc  42297  elbigo2r  42347  setrec2lem1  42440