MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq1d Unicode version

Theorem breq1d 4462
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1
Assertion
Ref Expression
breq1d

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2
2 breq1 4455 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  eqbrtrd  4472  syl6eqbr  4489  sbcbr2g  4508  pofun  4821  dffv2  5946  fmptco  6064  isorel  6222  soisores  6223  soisoi  6224  isocnv  6226  isotr  6232  f1owe  6249  weniso  6250  caovordig  6480  caovordg  6482  caovord  6486  f1oweALT  6784  frxp  6910  xporderlem  6911  fnwelem  6915  reldmtpos  6982  brtpos  6983  tpostpos  6994  tposoprab  7010  ensn1g  7600  fndmeng  7612  xpsneng  7622  xpcomco  7627  pwdom  7689  snnen2o  7726  supgtoreq  7949  ordtypelem6  7969  ordtypelem7  7970  wdompwdom  8025  infdiffi  8095  r1sdom  8213  pm54.43  8402  prdom2  8405  indcardi  8443  alephordi  8476  cdalepw  8597  fin23lem26  8726  fin23lem23  8727  fin23lem22  8728  fin23lem27  8729  uniimadomf  8941  alephval2  8968  inar1  9174  nqereu  9328  ltrnq  9378  prlem934  9432  prlem936  9446  ltasr  9498  addgt0sr  9502  axpre-ltadd  9565  axpre-sup  9567  ltsubadd  10047  lesubadd  10049  ltaddsub2  10052  leaddsub2  10054  ltaddpos  10067  lesub2  10072  ltnegcon2  10079  lenegcon2  10082  addge01  10087  subge0  10090  suble0  10091  lesub0  10094  ltordlem  10103  mulgt1  10426  ltmulgt11  10427  gt0div  10433  ge0div  10434  ltmuldiv  10440  ltmuldiv2  10441  lemuldiv2  10450  ltrec  10451  lerec2  10458  ltdiv23  10461  lediv23  10462  addltmul  10799  avglt1  10801  avgle1  10803  avgle  10805  zlem1lt  10940  zgt0ge1  10942  rpnnen1lem5  11241  reexALT  11243  xrmin2  11408  xltnegi  11444  xmulval  11453  xlesubadd  11484  xmullem2  11486  nn0disj  11820  dfceil2  11968  uzenom  12075  seqf1olem1  12146  leexp2r  12223  sqlecan  12274  expmulnbnd  12298  hashbnd  12411  hashle00  12465  hashgt12el2  12482  hashf1  12506  seqcoll  12512  hashge3el3dif  12524  lswccatn0lsw  12607  swrdccatin2  12712  swrd2lsw  12890  2swrd2eqwrdeq  12891  shftfval  12903  shftfib  12905  shftfn  12906  2shfti  12913  shftidt2  12914  sqrlem1  13076  sqrlem2  13077  sqrlem6  13081  sqrlem7  13082  absdiflt  13150  absdifle  13151  lenegsq  13153  cau3lem  13187  limsupgle  13300  limsupgre  13304  clim  13317  rlim  13318  rlim2  13319  clim2  13327  clim0  13329  clim0c  13330  rlim0  13331  rlim0lt  13332  climi0  13335  ello1  13338  ello1mpt  13344  elo1  13349  lo1o1  13355  rlimclim1  13368  rlimclim  13369  climrlim2  13370  rlimuni  13373  climuni  13375  lo1res  13382  rlimresb  13388  rlimeq  13392  2clim  13395  climshftlem  13397  climshft  13399  climabs0  13408  o1co  13409  rlimcn1  13411  rlimcn2  13413  climcn1  13414  climcn2  13415  addcn2  13416  subcn2  13417  mulcn2  13418  o1of2  13435  o1rlimmul  13441  rlimdiv  13468  rlimno1  13476  isershft  13486  isercoll  13490  climsup  13492  climcau  13493  caucvgrlem  13495  caucvgrlem2  13497  caurcvg2  13500  caucvg  13501  caucvgb  13502  serf0  13503  iseraltlem2  13505  iseralt  13507  sumeq1  13511  sumeq2w  13514  sumeq2ii  13515  sumrb  13535  summolem2  13538  summo  13539  zsum  13540  o1fsum  13627  cvgcmp  13630  cvgcmpce  13632  isumshft  13651  climcndslem1  13661  geolim  13679  geolim2  13680  geoisum1c  13689  mertenslem1  13693  mertenslem2  13694  mertens  13695  ntrivcvg  13706  ntrivcvgn0  13707  ntrivcvgmullem  13710  prodeq1f  13715  prodeq2w  13719  prodeq2ii  13720  prodrblem2  13738  prodmolem2  13742  prodmo  13743  zprod  13744  fprodntriv  13749  sin01bnd  13920  cos01bnd  13921  rpnnen  13960  ruclem9  13971  ruclem12  13974  sadcaddlem  14107  gcddvds  14153  dvdssq  14198  isprm  14219  isprm2lem  14224  prmgt1  14236  prmn2uzge3  14237  isprm6  14250  isprm5  14253  odzdvds  14322  pclem  14362  pcprecl  14363  pcprendvds  14364  pcpremul  14367  pcval  14368  pceulem  14369  pczndvds  14388  pcelnn  14393  pc2dvds  14402  pcadd  14408  pcadd2  14409  pcmpt  14411  prmpwdvds  14422  prmreclem1  14434  prmreclem5  14438  prmreclem6  14439  4sqlem17  14479  vdwlem10  14508  ramval  14526  0ram  14538  ram0  14540  ramz2  14542  ramub1lem2  14545  imasaddfnlem  14925  imasvscafn  14934  imasleval  14938  mreexexlemd  15041  symggen  16495  oddvdsnn0  16568  oddvds  16571  odf1  16584  odf1o1  16592  odf1o2  16593  gexdvds  16604  sylow1lem3  16620  efginvrel2  16745  efgsfo  16757  efgredlemd  16762  efgredlem  16765  efgred  16766  gexexlem  16858  torsubg  16860  oddvdssubg  16861  lt6abl  16897  ablfacrplem  17116  ablfacrp  17117  ablfaclem3  17138  abvfval  17467  abvpropd  17491  evlslem2  18180  znf1o  18590  znidomb  18600  cygznlem1  18605  frlmup1  18832  islinds  18844  lindsss  18859  chfacfscmul0  19359  chfacfscmulfsupp  19360  chfacfpmmul0  19363  chfacfpmmulfsupp  19364  cayleyhamilton1  19393  cctop  19507  ordthmeolem  20302  csdfil  20395  ufilen  20431  ptcmplem2  20553  ptcmplem3  20554  cnextfvval  20565  prdsxmetlem  20871  blfvalps  20886  elblps  20890  elbl  20891  elbl3ps  20894  elbl3  20895  blres  20934  imasf1obl  20991  blcld  21008  comet  21016  stdbdmetval  21017  stdbdbl  21020  metcnp2  21045  txmetcnp  21050  dscopn  21094  ngptgp  21150  nlmvscn  21196  nrginvrcn  21200  nmoval  21222  nghmcn  21252  cnbl0  21281  cnblcld  21282  bl2ioo  21297  recld2  21319  icccmplem2  21328  addcnlem  21368  divcn  21372  elcncf  21393  elcncf2  21394  cncfi  21398  rescncf  21401  mulc1cncf  21409  cncfco  21411  cncfmet  21412  cnheiborlem  21454  cnheibor  21455  cnllycmp  21456  evth  21459  htpycc  21480  phtpycc  21491  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  nmoleub2lem2  21599  nmoleub3  21602  nmhmcn  21603  ipcau2  21677  ipcn  21686  lmmbr2  21698  lmmcvg  21700  lmmbrf  21701  fmcfil  21711  iscau2  21716  iscau4  21718  iscauf  21719  caucfil  21722  iscmet3lem3  21729  iscmet3lem1  21730  iscmet3lem2  21731  cfilresi  21734  cfilres  21735  caussi  21736  causs  21737  lmle  21740  lmclim  21741  bcthlem1  21763  bcthlem4  21766  bcth  21768  minveclem3b  21843  minveclem3  21844  minveclem4  21847  minveclem5  21848  minveclem7  21850  pmltpclem1  21860  pmltpc  21862  ivthlem1  21863  ivthlem2  21864  ivthlem3  21865  ivth  21866  cniccbdd  21873  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovoliunlem3  21915  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2lem5  21932  ioombl1lem4  21971  ioombl1  21972  uniioombllem6  21997  volsup2  22014  volcn  22015  mbfmulc2lem  22054  mbfsup  22071  mbflimsup  22073  itg1climres  22121  mbfi1fseqlem6  22127  mbfi1fseq  22128  mbfi1flimlem  22129  itg2leub  22141  itg2seq  22149  itg2mulclem  22153  itg2monolem1  22157  itg2mono  22160  itg2i1fseq  22162  itg2addlem  22165  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  bddmulibl  22245  itgcn  22249  ellimc3  22283  dveflem  22380  dvferm1lem  22385  dvferm2lem  22387  rolle  22391  dvlip  22394  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  c1lip3  22400  dvge0  22407  dvivthlem1  22409  lhop1lem  22414  lhop1  22415  dvcvx  22421  dvfsumabs  22424  dvfsumlem2  22428  dvfsumrlim  22432  ftc1a  22438  ftc1lem4  22440  ftc1lem6  22442  itgsubstlem  22449  mdegleb  22464  mdegmullem  22478  deg1lt0  22491  ply1divmo  22536  ply1divex  22537  ply1divalg2  22539  q1peqb  22555  fta1g  22568  dgrub  22631  coe1termlem  22655  dgrcolem2  22671  dgrco  22672  quotval  22688  plydivlem3  22691  plydivlem4  22692  plydivex  22693  plydivalg  22695  quotlem  22696  plyrem  22701  fta1  22704  aannenlem1  22724  aannenlem2  22725  aalioulem3  22730  aalioulem4  22731  aalioulem5  22732  aalioulem6  22733  aaliou  22734  aaliou2  22736  aaliou2b  22737  ulmval  22775  ulm2  22780  ulmclm  22782  ulmshftlem  22784  ulmcaulem  22789  ulmcau  22790  ulmss  22792  ulmcn  22794  ulmdvlem1  22795  ulmdvlem3  22797  mtestbdd  22800  iblulm  22802  itgulm  22803  radcnvlem1  22808  pserulm  22817  abelthlem2  22827  abelthlem5  22830  abelthlem7  22833  abelthlem8  22834  abelthlem9  22835  abelth  22836  pilem3  22848  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  logltb  22984  logcnlem5  23027  cxpcn3lem  23121  cxpcn3  23122  cxpaddle  23126  logreclem  23150  rlimcnp  23295  rlimcnp2  23296  xrlimcnp  23298  rlimcxp  23303  cxploglim  23307  jensen  23318  emcllem6  23330  emcllem7  23331  ftalem2  23347  ftalem3  23348  ftalem5  23350  sqfpc  23411  mumullem2  23454  sqff1o  23456  chtublem  23486  chtub  23487  fsumvma2  23489  chpchtsum  23494  logexprlim  23500  bposlem6  23564  lgslem2  23572  lgslem3  23573  lgsval  23575  lgsfcl2  23577  lgsfle1  23580  lgsle1  23586  lgsdirprm  23604  chtppilimlem2  23659  chtppilim  23660  dchrisumlema  23673  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  dchrisum  23677  dchrmusumlema  23678  dchrvmasumlem2  23683  dchrisum0flblem1  23693  dchrisum0lema  23699  2vmadivsumlem  23725  chpdifbndlem1  23738  selberg3lem1  23742  selberg4lem1  23745  pntrsumbnd  23751  pntrsumbnd2  23752  selbergsb  23760  pntrlog2bndlem3  23764  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemn  23785  pntlemj  23788  pntlemi  23789  pntlemo  23792  pntlem3  23794  pntlemp  23795  pntleml  23796  pnt3  23797  padicabv  23815  ostth2lem2  23819  ostth3  23823  ostth  23824  mirbtwnhl  24060  foot  24096  footeq  24098  mideulem2  24108  opphllem6  24124  hpgbr  24129  lmieu  24150  iscgra  24169  brbtwn2  24208  colinearalg  24213  axcontlem10  24276  umgrale  24321  umgrafi  24322  umgra1  24326  uslgra1  24372  1pthoncl  24594  2pthoncl  24605  clwlkisclwwlk2  24790  0eusgraiff0rgra  24939  umgrabi  24983  frgrawopreglem2  25045  isnvlem  25503  nvelbl  25599  nvelbl2  25600  nmoofval  25677  nmosetn0  25680  nmoolb  25686  nmoubi  25687  nmounbseqi  25692  nmounbseqiOLD  25693  nmobndseqi  25694  nmobndseqiOLD  25695  bloval  25696  isblo  25697  nmoo0  25706  nmlno0lem  25708  blocnilem  25719  siilem2  25767  ubthlem1  25786  ubthlem2  25787  ubthlem3  25788  ubth  25789  minvecolem3  25792  minvecolem4  25796  minvecolem5  25797  minvecolem7  25799  htthlem  25834  htth  25835  h2hcau  25896  h2hlm  25897  normlem7tALT  26036  norm3lemt  26069  hcau  26101  hlimi  26105  hlim2  26109  cmcm3  26533  pjnorm  26642  pjnel  26644  elcnop  26776  elbdop  26779  nmopsetn0  26784  nmfnsetn0  26797  elcnfn  26801  hhcno  26823  hhcnf  26824  nmoplb  26826  nmopub  26827  cnopc  26832  nmfnlb  26843  nmfnleub  26844  cnfnc  26849  idcnop  26900  nmop0  26905  nmfn0  26906  nmlnop0iALT  26914  nmcexi  26945  nmcopexi  26946  lnconi  26952  lnopcon  26954  nmcfnexi  26970  lnfncon  26975  branmfn  27024  leop3  27044  opsqrlem6  27064  cvmd  27255  cvdmd  27256  cvexch  27293  cdj3i  27360  fmptcof2  27502  xraddge02  27577  xdivpnfrp  27629  omndadd  27696  omndmul  27704  archirngz  27733  archiabllem2a  27738  isorng  27789  locfinreflem  27843  locfinref  27844  sqsscirc2  27891  cnre2csqlem  27892  xrge0iifiso  27917  lmdvg  27935  qqhcn  27972  qqhucn  27973  brfae  28220  dya2ub  28241  oddpwdc  28293  eulerpartlemd  28305  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemimin  28444  ballotlemic  28445  ballotlemsv  28448  ballotlemfrcn0  28468  ballotlemrc  28469  sgnmul  28481  sgnmulsgn  28488  signsply0  28508  signswch  28518  signsvfn  28539  signsvfnn  28543  signlem0  28544  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgamgulmlem6  28576  lgambdd  28579  lgamucov  28580  lgamcvglem  28582  erdszelem8  28642  kur14  28660  snmlval  28776  snmlflim  28777  sinccvg  29039  abs2sqle  29046  abs2sqlt  29047  faclim2  29173  poseq  29333  soseq  29334  sltval  29407  brimg  29587  cgrtriv  29652  cgrdegen  29654  brofs  29655  cgrextend  29658  segconeu  29661  fvtransport  29682  transportprops  29684  brifs  29693  ifscgr  29694  brcgr3  29696  cgrxfr  29705  brfs  29729  btwnconn1lem7  29743  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem14  29750  brsegle  29758  segleantisym  29765  outsideofeu  29781  nndivlub  29923  heicant  30049  dvtanlem  30064  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  bddiblnc  30085  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anc  30098  areacirclem1  30107  areacirclem2  30108  areacirclem4  30110  areacirclem5  30111  areacirc  30112  nn0prpwlem  30140  nn0prpw  30141  seqpo  30240  incsequz2  30242  lmclim2  30251  geomcau  30252  caushft  30254  prdsbnd  30289  ismtyima  30299  heiborlem4  30310  heiborlem6  30312  heiborlem7  30313  bfplem1  30318  bfplem2  30319  rrndstprj2  30327  rrncmslem  30328  rrnequiv  30331  irrapxlem3  30760  irrapxlem4  30761  irrapxlem5  30762  irrapxlem6  30763  pellexlem3  30767  monotoddzz  30879  jm2.19  30935  rmydioph  30956  fnwe2lem2  30997  hbtlem1  31072  hbtlem2  31073  hbtlem7  31074  hbtlem4  31075  hbtlem5  31077  hbtlem6  31078  dgrsub2  31084  fiuneneq  31154  isprm7  31192  lcmgcdlem  31212  lcmdvds  31214  nzss  31222  evth2f  31390  evthf  31402  cncmpmax  31407  rfcnpre4  31409  fmul01  31574  climinf  31612  climsuse  31614  mullimc  31622  ellimcabssub0  31623  climf  31628  mullimcf  31629  idlimc  31632  limcperiod  31634  clim2f  31642  limsupre  31647  limcleqr  31650  limclner  31657  clim0cf  31660  cncfshift  31676  cncfperiod  31681  fperdvper  31715  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem7  31789  stoweidlem9  31791  stoweidlem15  31797  stoweidlem16  31798  stoweidlem18  31800  stoweidlem21  31803  stoweidlem26  31808  stoweidlem31  31813  stoweidlem34  31816  stoweidlem36  31818  stoweidlem37  31819  stoweidlem41  31823  stoweidlem44  31826  stoweidlem45  31827  stoweidlem46  31828  stoweidlem48  31830  stoweidlem51  31833  stoweidlem52  31834  stoweidlem55  31837  stoweidlem59  31841  stoweidlem60  31842  fourierdlem20  31909  fourierdlem25  31914  fourierdlem37  31926  fourierdlem39  31928  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem54  31943  fourierdlem64  31953  fourierdlem68  31957  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem79  31968  fourierdlem80  31969  fourierdlem87  31976  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem103  31992  fourierdlem104  31993  fourierdlem105  31994  fourierdlem108  31997  fourierdlem109  31998  fourierdlem111  32000  fourierswlem  32013  fouriersw  32014  etransclem31  32048  etransclem47  32064  etransclem48  32065  etransc  32066  pgrpgt2nabl  32959  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  oposlem  34907  opltcon2b  34931  pats  35010  ishlat1  35077  cvrexch  35144  atle  35160  athgt  35180  1cvrco  35196  3atlem5  35211  4atlem3  35320  dalawlem15  35609  lhprelat3N  35764  lautle  35808  lautcvr  35816  ltrnatb  35861  ltrneq2  35872  cdlemefr32sn2aw  36130  cdlemefs32sn1aw  36140  cdleme32fvaw  36165  cdleme35sn3a  36185  cdleme46frvlpq  36230  cdleme48gfv  36263  trlord  36295  cdlemg1fvawlemN  36299  cdlemg7fvbwN  36333  cdlemg31d  36426  istendo  36486  dva1dim  36711  dvhb1dimN  36712  diafval  36758  diaelval  36760  cdlemm10N  36845  dihopelvalcpre  36975  dihmeetcN  37029  dihmeetlem6  37036  dihjatc1  37038  rp-isfinite5  37743  leeq1d  37969  extoimad  37981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator