Theorem breq1 4926

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2050  ⟨cop 4441   class class class wbr 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924

This theorem is referenced by:  breq12  4928  breq1i  4930  breq1d  4933  nbrne2  4943  brab1  4971  pocl  5327  swopolem  5329  swopo  5330  po2ne  5335  solin  5344  sotrieq  5348  sotr2  5351  isso2i  5354  somo  5356  frirr  5378  fr2nr  5379  wereu2  5398  vtoclr  5459  frsn  5483  brcog  5581  brcogw  5583  brcnvg  5594  dfdmf  5609  eldmg  5611  dfrnf  5657  dfres2  5748  imasng  5785  asymref2  5811  sotri2  5823  somin1  5827  coi1  5948  dffun6f  6196  funmo  6198  fun11  6255  fveq2  6493  eliman0  6529  nfunsn  6531  dffv2  6578  fvopab5  6619  dff3  6683  f1ompt  6692  fmptco  6708  dff13  6832  foeqcnvco  6875  isorel  6896  soisores  6897  soisoi  6898  isocnv  6900  isotr  6906  isomin  6907  isoini  6908  isopolem  6915  isosolem  6917  f1oiso  6921  f1oiso2  6922  weniso  6924  caovordig  7163  caovordg  7165  caovord3d  7168  caovord  7169  caovord3  7171  caofrss  7254  caoftrn  7256  fr3nr  7304  dfwe2  7306  f1oweALT  7479  frxp  7619  poxp  7621  fnse  7626  brtpos2  7695  rntpos  7702  tpostpos  7709  ertr  8098  ecopovsym  8193  ecopovtrn  8194  isfi  8324  en0  8363  en1  8367  endisj  8394  xpcomco  8397  sbth  8427  2pwne  8463  disjenex  8465  ssenen  8481  nneneq  8490  php  8491  sdom1  8507  isinf  8520  fineqvlem  8521  pssnn  8525  en1eqsnbi  8538  enp1i  8542  findcard  8546  findcard2  8547  findcard3  8550  frfi  8552  fiint  8584  mapfienlem1  8657  mapfienlem2  8658  mapfienlem3  8659  mapfien  8660  marypha1lem  8686  supmo  8705  eqsup  8709  supub  8712  suplub  8713  suppr  8724  supisolem  8726  supisoex  8727  infmin  8747  infmo  8748  fiinfg  8752  fiinf2g  8753  infpr  8756  ordtypecbv  8770  ordtypelem3  8773  ordtypelem6  8776  ordtypelem7  8777  ordtypelem9  8779  ordtypelem10  8780  hartogslem1  8795  hartogs  8797  wemaplem1  8799  wemaplem2  8800  wemapso2lem  8805  card2on  8807  card2inf  8808  elharval  8816  brwdom2  8826  wdomtr  8828  cantnfs  8917  cantnfp1lem2  8930  oemapso  8933  cantnflem1  8940  wemapwe  8948  r111  8992  kardex  9111  karden  9112  isnumi  9163  tskwe  9167  cardid2  9170  cardonle  9174  cardne  9182  iscard2  9193  infxpenlem  9227  fodomfi2  9274  wdomfil  9275  wdomnumr  9278  alephsuc2  9294  infenaleph  9305  iunfictbso  9328  infpss  9431  cff1  9472  cfslb2n  9482  sornom  9491  fin4i  9512  isfin6  9514  isfin7  9515  isfin1-3  9600  fin1a2lem9  9622  fin1a2lem11  9624  hsmexlem4  9643  axcc2lem  9650  axcc4dom  9655  domtriomlem  9656  numthcor  9708  zorn2lem2  9711  zorn2lem3  9712  zorn2lem7  9716  zorn2g  9717  axdclem  9733  axdc  9735  brdom7disj  9745  brdom6disj  9746  uniimadom  9758  ondomon  9777  alephval2  9786  alephreg  9796  pwcfsdom  9797  elgch  9836  gchi  9838  fpwwe2lem12  9855  fpwwe2lem13  9856  pwfseqlem4  9876  winainflem  9907  winalim2  9910  tsken  9968  0tsk  9969  inar1  9989  tskord  9994  tskuni  9997  grudomon  10031  pinq  10141  nqereu  10143  enqeq  10148  ltbtwnnq  10192  ltrnq  10193  prcdnq  10207  prnmax  10209  genpnmax  10221  nqpr  10228  1idpr  10243  reclem2pr  10262  reclem3pr  10263  reclem4pr  10264  recexpr  10265  supexpr  10268  ltsosr  10308  1ne0sr  10310  ltasr  10314  supsrlem  10325  axpre-lttri  10379  axpre-lttrn  10380  axpre-ltadd  10381  axpre-sup  10383  lelttr  10525  dedekind  10597  dedekindle  10598  ltordlem  10960  lt0ne0d  11000  fimaxre3  11382  fiminreOLD  11385  lbreu  11386  lble  11388  sup2  11392  infm3  11395  suprleub  11402  supaddc  11403  supadd  11404  supmul1  11405  supmullem1  11406  supmul  11408  nnne0  11468  nnsub  11478  nominpos  11678  nnunb  11697  arch  11698  nn0sub  11753  nn0n0n1ge2b  11769  nn0lt10b  11851  zextle  11862  peano5uzti  11879  fzind  11887  btwnz  11891  uzval  12054  uzwo  12119  nnwof  12122  ublbneg  12141  lbzbi  12144  zsupss  12145  uzsupss  12148  uzwo3  12151  zmax  12153  rebtwnz  12155  rpnnen1lem3  12187  xrltnsym  12341  xrlttri  12343  xrlttr  12344  xrlelttr  12360  nltpnft  12368  xrmaxlt  12385  xrmaxle  12387  qbtwnre  12403  qbtwnxr  12404  xltnegi  12420  xnn0lenn0nn0  12448  xsubge0  12464  xlesubadd  12466  xmullem2  12468  xlemul1a  12491  xrinfmexpnf  12509  xrsupsslem  12510  xrinfmsslem  12511  xrub  12515  supxrunb1  12522  supxrunb2  12523  reltre  12543  rpltrp  12544  reltxrnmnf  12545  ixxval  12556  elixx1  12557  elioo2  12589  iccid  12593  icc0  12596  fzval  12704  elfz1  12707  elfznelfzo  12951  elfznelfzob  12952  flval  12973  fllelt  12976  flflp1  12986  flval2  12993  flval3  12994  flbi  12995  dfceil2  13018  ceilval2  13019  fleqceilz  13031  modid2  13075  addmodlteq  13123  fsequb2  13153  ssnn0fi  13162  seqf1olem2  13219  sqlecan  13380  faclbnd4lem1  13462  hashsnle1  13585  pr2pwpr  13642  swrdccatidOLD  13942  rtrclreclem3  14274  relexpindlem  14277  sgnval  14302  sqrlem6  14462  01sqrex  14464  abslt  14529  absle  14530  rexanre  14561  rexico  14568  limsupgle  14689  limsupgre  14693  limsupbnd2  14695  rlim2lt  14709  rlim3  14710  ello12r  14729  ello1d  14735  elo12r  14740  rlimconst  14756  climshft  14788  rlimcn2  14802  o1rlimmul  14830  lo1le  14863  climsup  14881  caucvgrlem  14884  isumless  15054  divrcnv  15061  cvgrat  15093  rpnnen2lem10  15430  ruclem1  15438  ruclem2  15439  ruclem11  15447  ruclem12  15448  sqrt2irr  15456  absdvdsb  15482  dvdsle  15514  dvdsabseq  15517  dvdsdivcl  15520  dvdsext  15525  divalglem8  15605  divalglem9  15606  divalglem10  15607  divalgmod  15611  ndvdssub  15614  sadcaddlem  15660  gcdcllem1  15702  gcdcllem2  15703  gcdcllem3  15704  dfgcd2  15744  gcdzeq  15752  dvdssq  15761  nn0seqcvgd  15764  algcvgblem  15771  lcmval  15786  lcmdvds  15802  lcmgcdeq  15806  lcmfpr  15821  lcmf  15827  lcmftp  15830  lcmfunsnlem1  15831  lcmfunsnlem2lem1  15832  lcmfunsnlem2lem2  15833  lcmfdvdsb  15837  coprmgcdb  15843  coprmdvds1  15846  1nprm  15873  1idssfct  15874  isprm2lem  15875  isprm2  15876  dvdsprime  15881  nprm  15882  3prm  15888  dvdsprm  15897  exprmfct  15898  isprm5  15901  maxprmfct  15903  coprm  15905  ncoprmlnprm  15918  eulerthlem2  15969  phisum  15977  odzval  15978  pythagtriplem4  16006  pc2dvds  16065  pcprmpw2  16068  pcprmpw  16069  dvdsprmpweqle  16072  oddprmdvds  16089  prmpwdvds  16090  pockthg  16092  unbenlem  16094  prmreclem4  16105  prmreclem5  16106  prmreclem6  16107  1arith  16113  vdwlem6  16172  vdwlem11  16177  vdwlem13  16179  ramtlecl  16186  ramub  16199  rami  16201  ramubcl  16204  0ram  16206  ram0  16208  prmdvdsprmop  16229  prmolefac  16232  prmodvdslcmf  16233  prmgaplem2  16236  prmgaplcmlem1  16237  prmgaplcmlem2  16238  prmgaplem3  16239  prmgaplem4  16240  prmgaplem5  16241  prmgaplem6  16242  prmgapprmolem  16247  prmlem0  16289  prmlem1a  16290  imasaddfnlem  16651  imasvscafn  16660  imasleval  16664  prslem  17393  drsdir  17397  drsdirfi  17400  isdrs2  17401  posi  17412  posasymb  17414  pltval3  17429  plelttr  17434  pospo  17435  lubprop  17448  luble  17449  lublecllem  17450  glbprop  17461  joinval2lem  17470  joinlem  17473  meetlem  17487  meetle  17490  latnlej  17530  isglbd  17579  lubub  17581  lubun  17585  clatleglb  17588  pospropd  17596  poslubmo  17608  posglbmo  17609  poslubd  17610  tsrlin  17681  letsr  17689  dirge  17699  pmtrval  18334  pmtrrn  18340  pmtrfrn  18341  pmtrrn2  18343  pmtrsn  18403  mndodcongi  18427  odeq  18434  odmulgeq  18439  gexnnod  18468  sylow1lem1  18478  pgpssslw  18494  sylow2a  18499  efgredeu  18632  efgred2  18633  gexex  18723  frgpnabllem2  18744  cyggenod  18753  dprdval  18869  dprdw  18876  dprdwd  18877  ablfacrplem  18931  ablfac1c  18937  ablfac1eu  18939  ablfaclem3  18953  abvtrivd  19327  psrbagconcl  19861  psrbagconf1o  19862  gsumbagdiaglem  19863  psrmulcllem  19875  psrlidm  19891  psrridm  19892  psrass1  19893  psrcom  19897  mplelbas  19918  mplmonmul  19952  ltbwe  19960  coe1fsupp  20079  coe1ae0  20081  coe1mul2  20134  coe1tmmul  20142  zringlpir  20332  prmirredlem  20336  znleval  20397  frlmelbas  20596  ellspd  20642  islindf4  20678  pmatcoe1fsupp  21007  chfacffsupp  21162  chfacfscmulfsupp  21165  chfacfscmulgsum  21166  chfacfpmmulfsupp  21169  chfacfpmmulgsum  21170  ordtbas2  21497  ordtopn2  21501  ordtrest2lem  21509  pnfnei  21526  ordtt1  21685  ordthauslem  21689  2ndci  21754  2ndcsb  21755  2ndcredom  21756  2ndc1stc  21757  1stcrest  21759  2ndcctbss  21761  2ndcdisj  21762  2ndcsep  21765  lly1stc  21802  tx1stc  21956  ordthmeolem  22107  ufildom1  22232  xmetrtri2  22663  prdsxmetlem  22675  ssblex  22735  prdsbl  22798  comet  22820  stdbdxmet  22822  stdbdmopn  22825  met1stc  22828  dscmet  22879  metdstri  23156  metdscn  23161  xrhmeo  23247  bndth  23259  evth  23260  lebnumlem3  23264  pcovalg  23313  pco1  23316  pcocn  23318  pcopt  23323  pcopt2  23324  pcoass  23325  nmoleub3  23420  bcthlem5  23628  rrxfsupp  23702  minveclem4c  23725  minveclem2  23726  minveclem3b  23728  minveclem4  23732  minveclem6  23734  pmltpclem1  23746  pmltpc  23748  ovollb2lem  23786  ovolctb  23788  ovolunlem1  23795  ovoliunlem1  23800  ovoliunlem2  23801  ovoliun2  23804  ovolshftlem1  23807  ovolscalem1  23811  ovolicc1  23814  ovolicc2lem3  23817  voliunlem2  23849  voliunlem3  23850  ioombl1lem4  23859  uniioovol  23877  uniioombllem2  23881  uniioombllem3  23883  uniioombllem6  23886  volsup2  23903  ismbfd  23937  mbfsup  23962  mbflimsup  23964  itg1climres  24012  mbfi1fseqlem4  24016  itg2lr  24028  itg2leub  24032  itg2seq  24040  itg2monolem1  24048  itg2monolem3  24050  itg2mono  24051  itg2i1fseq2  24054  itg2gt0  24058  itg2cnlem1  24059  itg2cnlem2  24060  itg2cn  24061  iblss  24102  itgless  24114  ibladdlem  24117  iblabsr  24127  iblmulc2  24128  itgabs  24132  ditgeq1  24143  dvferm2lem  24280  rolle  24284  dvlip2  24289  c1liplem1  24290  c1lip1  24291  dvfsumlem2  24321  dvfsumlem4  24323  mdegleb  24355  degltlem1  24363  plyco0  24479  plyeq0lem  24497  coeeq2  24529  dgrle  24530  dgradd2  24555  plydiveu  24584  aareccl  24612  aalioulem2  24619  aaliou3lem7  24635  psercnlem1  24710  pilem2  24737  pilem3  24738  logltb  24878  divlogrlim  24913  logcnlem3  24922  cxpaddlelem  25027  rlimcnp  25239  cxplim  25245  cxploglim  25251  scvxcvx  25259  ftalem1  25346  ftalem2  25347  isppw2  25388  vmappw  25389  sgmnncl  25420  sqff1o  25455  fsumdvdsdiaglem  25456  dvdsppwf1o  25459  dvdsflsumcom  25461  musum  25464  muinv  25466  dvdsmulf1o  25467  vmalelog  25477  vmasum  25488  logfac2  25489  perfectlem2  25502  bcmono  25549  bpos1lem  25554  bposlem9  25564  lgsmod  25595  lgsne0  25607  gausslemma2dlem4  25641  2sqlem6  25695  2sqlem8  25698  2sqlem10  25700  2sqreulem1  25718  2sqreunnlem1  25721  chtppilim  25747  rpvmasumlem  25759  dchrisumlema  25760  dchrisumlem2  25762  dchrvmasumlem1  25767  dchrvmasumiflem1  25773  dchrisum0flblem1  25780  dchrisum0flblem2  25781  dchrisum0  25792  rplogsum  25799  logsqvma  25814  pntpbnd1  25858  pntpbnd2  25859  pntibndlem3  25864  pntlemj  25875  pntlemi  25876  pntlem3  25881  pnt3  25884  ostth3  25910  tgjustc1  25957  tgjustc2  25958  iscgrglt  25996  tgcgr4  26013  hlcgreu  26100  lmif  26267  islmib  26269  trgcopyeu  26288  iscgrad  26293  inaghl  26328  axlowdim2  26443  axlowdim  26444  axcontlem2  26448  axcontlem3  26449  axcontlem4  26450  axcontlem7  26453  axcontlem9  26455  axcontlem10  26456  axcontlem11  26457  axcontlem12  26458  ebtwntg  26465  umgrupgr  26585  nbusgrvtxm1  26858  crctcshwlkn0lem2  27291  crctcshwlkn0lem3  27292  crctcsh  27304  wlkswwlksf1o  27359  clwlkclwwlklem2fv1  27495  clwlkclwwlkfOLD  27512  clwlkclwwlkf  27516  0clwlkv  27654  eupth2  27763  numclwwlk5  27939  nmoubi  28320  minvecolem2  28424  minvecolem3  28425  minvecolem4c  28428  minvecolem4  28429  minvecolem5  28430  minvecolem6  28431  htthlem  28467  chlimi  28784  chcompl  28792  hsn0elch  28798  cmbr3  29160  cmcm  29166  cmcm3  29167  lecm  29169  nmopub  29460  nmfnleub  29477  nmopun  29566  nmcexi  29578  cnlnadjlem7  29625  pjnmopi  29700  stle0i  29791  stlesi  29793  stm1i  29795  csmdsymi  29886  cvmd  29888  atcveq0  29900  atcv1  29932  atord  29940  atcvat2  29941  chirred  29947  mdsym  29964  mddmdin0i  29983  cdj1i  29985  fmptcof2  30158  fnpreimac  30172  isoun  30190  fcobijfs  30212  lt2addrd  30228  xlt2addrd  30235  xrge0infss  30237  infxrge0glb  30242  xrofsup  30245  fz1nnct  30274  tleile  30380  toslublem  30386  tosglblem  30388  omndadd  30425  xrnarchi  30479  archirng  30483  archiexdiv  30485  archiabl  30493  isarchiofld  30569  linds2eq  30612  lbsdiflsp0  30651  fedgmullem1  30654  fedgmullem2  30655  fedgmul  30656  psgnfzto1stlem  30691  fzto1st  30694  psgnfzto1st  30696  smatrcl  30703  smatlem  30704  madjusmdetlem2  30735  madjusmdet  30738  cmpcref  30758  ldlfcntref  30762  dispcmp  30767  ordtrest2NEWlem  30809  ordtconnlem1  30811  xrge0iifiso  30822  rge0scvg  30836  gsumesum  30962  esumfsup  30973  esumpinfval  30976  esumpcvgval  30981  esumcvg  30989  sigaclcu  31021  sigaclci  31036  unelsiga  31038  unelldsys  31062  sigapildsys  31066  ldgenpisyslem1  31067  fiunelros  31078  measvun  31113  voliune  31133  volfiniune  31134  oms0  31200  omssubaddlem  31202  omssubadd  31203  carsgsigalem  31218  carsgclctunlem2  31222  carsgclctun  31224  pmeasmono  31227  pmeasadd  31228  orvcval2  31362  dstfrvel  31377  ballotlemfc0  31396  ballotlemfcc  31397  ballotlemsv  31413  ballotlemsf1o  31417  sgnmulsgn  31453  breprexp  31552  tgoldbachgt  31582  bnj23  31636  bnj1185  31713  bnj1152  31915  bnj1418  31957  eqfunresadj  32524  dfdm5  32536  dfrn5  32537  trpredpred  32588  frpomin  32599  poseq  32616  wzel  32632  wsuclem  32633  frrlem12  32655  nodense  32717  noresle  32721  noprefixmo  32723  nosupdm  32725  nosupbnd1lem1  32729  nosupbnd1lem4  32732  nosupbnd1  32735  nosupbnd2lem1  32736  nosupbnd2  32737  noetalem5  32742  nocvxminlem  32768  conway  32785  scutval  32786  etasslt  32795  slerec  32798  madeval2  32811  brpprod  32867  brsset  32871  brbigcup  32880  dffix2  32887  elfuns  32897  brimageg  32909  brdomaing  32917  brrangeg  32918  brimg  32919  brapply  32920  brsuccf  32923  funpartlem  32924  brrestrict  32931  dfrecs2  32932  dfrdg4  32933  brofs  32987  btwncomim  32995  btwnintr  33001  btwnexch3  33002  btwnexch2  33005  brifs  33025  brcolinear2  33040  colineardim1  33043  brfs  33061  btwnconn1  33083  segcon2  33087  seglerflx  33094  seglemin  33095  btwnsegle  33099  colinbtwnle  33100  broutsideof2  33104  fvray  33123  lineunray  33129  lineelsb2  33130  linerflx1  33131  trer  33185  elicc3  33186  finminlem  33187  nn0prpwlem  33191  nn0prpw  33192  fnessref  33226  refssfne  33227  unblimceq0lem  33365  unblimceq0  33366  unbdqndv2  33370  knoppndvlem21  33391  taupilemrplb  34043  dfgcd3  34047  icorempo  34074  icoreval  34076  iooelexlt  34085  relowlssretop  34086  domalom  34126  ctbssinf  34128  pibt2  34139  phpreu  34317  fin2solem  34319  fin2so  34320  ltflcei  34321  ptrecube  34333  poimirlem1  34334  poimirlem2  34335  poimirlem5  34338  poimirlem6  34339  poimirlem7  34340  poimirlem9  34342  poimirlem12  34345  poimirlem22  34355  poimirlem23  34356  poimirlem24  34357  poimirlem26  34359  poimirlem27  34360  poimirlem32  34365  heicant  34368  mblfinlem1  34370  mblfinlem2  34371  itg2addnclem  34384  itg2addnclem3  34386  itg2addnc  34387  itg2gt0cn  34388  ibladdnclem  34389  iblmulc2nc  34398  itgabsnc  34402  bddiblnc  34403  ftc1anclem5  34412  ftc1anclem7  34414  ftc1anclem8  34415  ftc1anc  34416  indexdom  34451  filbcmb  34457  fdc  34462  prdsbnd  34513  heiborlem3  34533  rrnequiv  34555  rngoueqz  34660  inxprnres  34993  eqvreltr  35287  prtlem10  35446  lsatcveq0  35613  lsatcv1  35629  oposlem  35763  opnlen0  35769  lub0N  35770  glb0N  35774  omllaw  35824  cmtbr4N  35836  cvrval  35850  cvrnbtwn  35852  cvrnbtwn2  35856  cvrnbtwn3  35857  cvrcon3b  35858  cvrnbtwn4  35860  atcvreq0  35895  atnle  35898  atlatmstc  35900  cvlexch1  35909  glbconN  35958  hlsuprexch  35962  exatleN  35985  cvratlem  36002  atcvrj0  36009  atcvrj2b  36013  atlelt  36019  cvrat4  36024  3dim1lem5  36047  3dim2  36049  3dim3  36050  ps-2  36059  llni  36089  llnn0  36097  llnle  36099  lplni  36113  lplni2  36118  lplnle  36121  lplnn0N  36128  llncvrlpln  36139  2llnjN  36148  lvoli  36156  lvoli3  36158  lvoli2  36162  lvoln0N  36172  4at  36194  lplncvrlvol  36197  2lplnj  36201  dalemcea  36241  dalem3  36245  psubspi  36328  linepsubN  36333  elpmap  36339  pmapsub  36349  lnatexN  36360  cdlema1N  36372  cdlemb  36375  elpadd  36380  paddvaln0N  36382  paddasslem5  36405  llnexchb2lem  36449  llnexch2N  36451  islhp  36577  lhpat3  36627  4atexlemex2  36652  4atex  36657  4atex2-0aOLDN  36659  4atex2-0cOLDN  36661  lautle  36665  lautcvr  36673  lauteq  36676  ldilval  36694  ltrnu  36702  trlval2  36744  trlne  36766  cdleme0ex1N  36804  cdleme0nex  36871  cdleme18d  36876  cdlemednuN  36881  cdleme25b  36935  cdleme25cv  36939  cdleme27b  36949  cdleme29b  36956  cdleme31sn  36961  cdleme31fv  36971  cdleme31fv2  36974  cdlemefrs29bpre0  36977  cdlemefr29bpre0N  36987  cdlemefr29clN  36988  cdlemefr32fvaN  36990  cdlemefr32fva1  36991  cdlemefs29pre00N  36993  cdlemefs32sn1aw  36995  cdlemefs29bpre0N  36997  cdlemefs29bpre1N  36998  cdlemefs29cpre1N  36999  cdlemefs29clN  37000  cdlemefs32fvaN  37003  cdlemefs32fva1  37004  cdleme41sn3a  37014  cdleme32fva  37018  cdleme32e  37026  cdleme35f  37035  cdleme40v  37050  cdleme42b  37059  trlord  37150  cdlemg1cex  37169  diaval  37613  diaeldm  37617  diaelrnN  37626  cdlemm10N  37699  dibglbN  37747  dicval  37757  dicfnN  37764  dicvalrelN  37766  dihval  37813  dihlsscpre  37815  dihglblem3N  37876  dihmeetlem2N  37880  djhcvat42  37996  qsalrel  38570  lzenom  38762  fphpdo  38810  irrapxlem4  38818  pellexlem6  38827  infmrgelbi  38871  pellfundre  38874  pellfundlb  38877  monotoddzz  38936  zindbi  38939  jm2.27  39001  rmydioph  39007  rpnnen3lem  39024  fnwe2lem2  39047  aomclem8  39057  hbtlem5  39124  hbt  39126  refimssco  39329  rfovfvfvd  39712  rfovcnvf1od  39713  fsovrfovd  39718  nzss  40065  wessf1ornlem  40869  axccdom  40912  dmrelrnrel  40915  axccd  40921  rnmptlb  40941  rnmptbdd  40943  rnmptbd2  40949  rnmptbdlem  40955  rnmptbd  40956  dstregt0  40976  suplesup  41036  fiminre2  41075  supxrunb3  41102  supxrleubrnmpt  41110  rexabslelem  41123  rexabsle  41124  suprleubrnmpt  41127  infrnmptle  41128  infxrunb3rnmpt  41133  infxrpnf  41152  supminfxr  41171  infrpgernmpt  41172  xrpnf  41193  limsupre  41353  limsupref  41397  limsupbnd1f  41398  limsuppnfd  41414  climinf2  41419  limsuppnf  41423  climinfmpt  41427  climinf3  41428  limsupmnflem  41432  limsupmnf  41433  limsupre2  41437  limsupmnfuzlem  41438  limsupre2mpt  41442  limsupre3lem  41444  limsupre3  41445  limsupre3mpt  41446  limsupre3uzlem  41447  limsupre3uz  41448  limsupreuz  41449  limsupreuzmpt  41451  liminfval2  41480  liminfreuzlem  41514  liminfreuz  41515  xlimpnfxnegmnf  41526  cnrefiisplem  41541  xlimpnfv  41550  xlimpnf  41554  xlimpnfmpt  41556  dfxlim2  41560  icccncfext  41600  cncficcgt0  41601  ioodvbdlimc1lem2  41647  ioodvbdlimc2lem  41649  stoweidlem5  41721  stoweidlem20  41736  stoweidlem26  41742  stoweidlem28  41744  stoweidlem29  41745  stoweidlem34  41750  wallispilem3  41783  stirlinglem13  41802  fourierdlem41  41864  fourierdlem42  41865  fourierdlem51  41873  fourierdlem54  41876  salunicl  42032  saluncl  42033  salexct  42048  salexct2  42053  salexct3  42056  salgencntex  42057  salgensscntex  42058  sge0pnffigt  42109  meadjuni  42170  omeunile  42218  ovnlerp  42275  hoidifhspval  42321  ovolval5lem2  42366  salpreimagelt  42417  pimincfltioo  42427  salpreimagtge  42433  salpreimagtlt  42438  incsmf  42450  issmfgt  42464  smfpreimagt  42469  decsmf  42474  issmfge  42477  smfpimgtxr  42487  smfpreimage  42489  smfinflem  42522  smfinf  42523  funressnfv  42683  funressnvmo  42685  funressnvmoOLD  42686  funressnmo  42687  dfdfat2  42733  tz6.12-afv  42778  funressndmafv2rn  42828  tz6.12-afv2  42845  dfatcolem  42860  dfatco  42861  iccpartigtl  42955  iccpartgt  42959  icceuelpartlem  42967  iccpartnel  42970  sprsymrelfolem2  43023  goldbachthlem2  43076  odz2prm2pw  43093  fmtnoprmfac1  43095  fmtnoprmfac2  43097  fmtnofac2  43099  fmtno4prmfac  43102  fmtno4prm  43105  prmdvdsfmtnof1lem1  43114  31prm  43128  perfectALTVlem2  43255  nnsum3primes4  43321  nnsum3primesprm  43323  nnsum3primesgbe  43325  nnsum3primesle9  43327  nnsum4primeseven  43333  nnsum4primesevenALTV  43334  wtgoldbnnsum4prm  43335  bgoldbnnsum3prm  43337  bgoldbtbndlem4  43341  bgoldbtbnd  43342  tgblthelfgott  43348  tgoldbach  43350  assintop  43480  isassintop  43481  assintopcllaw  43483  ztprmneprm  43759  ply1mulgsumlem1  43807  ply1mulgsumlem2  43808  lco0  43849  lcoel0  43850  lincsumcl  43853  lincscmcl  43854  lcoss  43858  linindslinci  43870  lindslinindsimp1  43879  linds0  43887  el0ldep  43888  lindsrng01  43890  ldepspr  43895  islindeps2  43905  isldepslvec2  43907  zlmodzxzldep  43926  ldepsnlinc  43930  elbigo2r  43981  setrec2lem1  44163