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

Theorem breq1d 4165
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
breq1d  |-  ( ph  ->  ( A R C  <-> 
B R C ) )

Proof of Theorem breq1d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq1 4158 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   class class class wbr 4155
This theorem is referenced by:  eqbrtrd  4175  syl6eqbr  4192  sbcbr2g  4207  pofun  4462  dffv2  5737  fmptco  5842  isorel  5987  soisores  5988  soisoi  5989  isocnv  5991  isotr  5997  f1owe  6014  f1oweALT  6015  weniso  6016  caovordig  6193  caovordg  6195  caovord  6199  frxp  6394  xporderlem  6395  fnwelem  6399  reldmtpos  6425  brtpos  6426  tpostpos  6437  tposoprab  6453  th3qlem2  6949  ensn1g  7110  fndmeng  7121  xpsneng  7131  xpcomco  7136  pwdom  7197  ordtypelem6  7427  ordtypelem7  7428  wdompwdom  7481  infdiffi  7547  r1sdom  7635  pm54.43  7822  prdom2  7825  indcardi  7857  alephordi  7890  cdalepw  8011  fin23lem26  8140  fin23lem23  8141  fin23lem22  8142  fin23lem27  8143  uniimadomf  8355  alephval2  8382  inar1  8585  nqereu  8741  ltrnq  8791  prlem934  8845  prlem936  8859  ltasr  8910  addgt0sr  8914  axpre-ltadd  8977  axpre-sup  8979  ltsubadd  9432  lesubadd  9434  ltaddsub2  9437  leaddsub2  9439  ltaddpos  9452  lesub2  9457  ltnegcon2  9464  lenegcon2  9467  addge01  9472  subge0  9475  suble0  9476  lesub0  9478  ltordlem  9486  mulgt1  9803  ltmulgt11  9804  gt0div  9810  ge0div  9811  ltmuldiv  9814  ltmuldiv2  9815  lemuldiv2  9824  ltrec  9825  lerec2  9832  ltdiv23  9835  lediv23  9836  addltmul  10137  avglt1  10139  avgle1  10141  avgle  10143  zlem1lt  10261  rpnnen1lem5  10538  reexALT  10540  xrmin2  10700  xltnegi  10736  xmulval  10745  xlesubadd  10776  xmullem2  10778  uzenom  11233  seqf1olem1  11291  leexp2r  11366  sqlecan  11416  expmulnbnd  11440  hashbnd  11553  hashle00  11598  hashgt12el2  11612  hashf1  11635  seqcoll  11641  shftfval  11814  shftfib  11816  shftfn  11817  2shfti  11824  shftidt2  11825  sqrlem1  11977  sqrlem2  11978  sqrlem6  11982  sqrlem7  11983  absdiflt  12050  absdifle  12051  lenegsq  12053  cau3lem  12087  limsupgle  12200  limsupgre  12204  clim  12217  rlim  12218  rlim2  12219  clim2  12227  clim0  12229  clim0c  12230  rlim0  12231  rlim0lt  12232  climi0  12235  ello1  12238  ello1mpt  12244  elo1  12249  lo1o1  12255  rlimclim1  12268  rlimclim  12269  climrlim2  12270  rlimuni  12273  climuni  12275  lo1res  12282  rlimresb  12288  rlimeq  12292  2clim  12295  climshftlem  12297  climshft  12299  climabs0  12308  o1co  12309  rlimcn1  12311  rlimcn2  12313  climcn1  12314  climcn2  12315  addcn2  12316  subcn2  12317  mulcn2  12318  o1of2  12335  o1rlimmul  12341  rlimdiv  12368  rlimno1  12376  isershft  12386  isercoll  12390  climsup  12392  climcau  12393  caucvgrlem  12395  caucvgrlem2  12397  caurcvg2  12400  caucvg  12401  caucvgb  12402  serf0  12403  iseraltlem2  12405  iseralt  12407  sumeq1f  12411  sumeq2w  12415  sumeq2ii  12416  cbvsum  12418  sumrb  12436  summolem2  12439  summo  12440  zsum  12441  o1fsum  12521  cvgcmp  12524  cvgcmpce  12526  isumshft  12548  climcndslem1  12558  geolim  12576  geolim2  12577  geoisum1c  12586  mertenslem1  12590  mertenslem2  12591  mertens  12592  sin01bnd  12715  cos01bnd  12716  rpnnen  12755  ruclem9  12766  ruclem12  12769  sadcaddlem  12898  gcddvds  12944  dvdssq  12989  isprm  13010  isprm2lem  13015  isprm6  13038  isprm5  13041  odzdvds  13110  pclem  13141  pcprecl  13142  pcprendvds  13143  pcpremul  13146  pcval  13147  pceulem  13148  pczndvds  13167  pcelnn  13172  pc2dvds  13181  pcadd  13187  pcadd2  13188  pcmpt  13190  prmpwdvds  13201  prmreclem1  13213  prmreclem5  13217  prmreclem6  13218  4sqlem17  13258  vdwlem10  13287  ramval  13305  0ram  13317  ram0  13319  ramz2  13321  ramub1lem2  13324  imasaddfnlem  13682  imasvscafn  13691  imasleval  13695  mreexexlemd  13798  oddvdsnn0  15111  oddvds  15114  odf1  15127  odf1o1  15135  odf1o2  15136  gexdvds  15147  sylow1lem3  15163  efginvrel2  15288  efgsfo  15300  efgredlemd  15305  efgredlem  15308  efgred  15309  gexexlem  15396  torsubg  15398  oddvdssubg  15399  lt6abl  15433  ablfacrplem  15552  ablfacrp  15553  ablfaclem3  15574  abvfval  15835  abvpropd  15859  znf1o  16757  znidomb  16767  cygznlem1  16772  cctop  16995  ordthmeolem  17756  csdfil  17849  ufilen  17885  ptcmplem2  18007  ptcmplem3  18008  cnextfvval  18019  prdsxmetlem  18308  blfval  18323  elbl  18325  elbl3  18327  blres  18353  imasf1obl  18410  blcld  18427  comet  18435  stdbdmetval  18436  stdbdbl  18439  metcnp2  18464  txmetcnp  18469  dscopn  18494  ngptgp  18550  nlmvscn  18596  nrginvrcn  18600  nmoval  18622  nghmcn  18652  cnbl0  18681  cnblcld  18682  bl2ioo  18696  recld2  18718  icccmplem2  18727  addcnlem  18767  divcn  18771  elcncf  18792  elcncf2  18793  cncfi  18797  rescncf  18800  mulc1cncf  18808  cncfco  18810  cncfmet  18811  cnheiborlem  18852  cnheibor  18853  cnllycmp  18854  evth  18857  htpycc  18878  phtpycc  18889  pcohtpylem  18917  pcoass  18922  pcorevlem  18924  nmoleub2lem2  18997  nmoleub3  19000  nmhmcn  19001  ipcau2  19064  ipcn  19073  lmmbr2  19085  lmmcvg  19087  lmmbrf  19088  fmcfil  19098  iscau2  19103  iscau4  19105  iscauf  19106  caucfil  19109  iscmet3lem3  19116  iscmet3lem1  19117  iscmet3lem2  19118  cfilresi  19121  cfilres  19122  caussi  19123  causs  19124  lmle  19127  lmclim  19128  bcthlem1  19148  bcthlem4  19151  bcth  19153  minveclem3b  19198  minveclem3  19199  minveclem4  19202  minveclem5  19203  minveclem7  19205  pmltpclem1  19214  pmltpc  19216  ivthlem1  19217  ivthlem2  19218  ivthlem3  19219  ivth  19220  cniccbdd  19227  ovolunlem1  19262  ovoliunlem1  19267  ovoliunlem2  19268  ovoliunlem3  19269  ovolshftlem1  19274  ovolscalem1  19278  ovolicc1  19281  ovolicc2lem3  19284  ovolicc2lem4  19285  ovolicc2lem5  19286  ioombl1lem4  19324  ioombl1  19325  uniioombllem6  19349  volsup2  19366  volcn  19367  mbfmulc2lem  19408  mbfsup  19425  mbflimsup  19427  itg1climres  19475  mbfi1fseqlem6  19481  mbfi1fseq  19482  mbfi1flimlem  19483  itg2leub  19495  itg2seq  19503  itg2mulclem  19507  itg2monolem1  19511  itg2mono  19514  itg2i1fseq  19516  itg2addlem  19519  itg2gt0  19521  itg2cnlem1  19522  itg2cnlem2  19523  itg2cn  19524  bddmulibl  19599  itgcn  19603  ellimc3  19635  dveflem  19732  dvferm1lem  19737  dvferm2lem  19739  rolle  19743  dvlip  19746  dvlipcn  19747  dvlip2  19748  c1liplem1  19749  c1lip3  19752  dvge0  19759  dvivthlem1  19761  lhop1lem  19766  lhop1  19767  dvcvx  19773  dvfsumabs  19776  dvfsumlem2  19780  dvfsumrlim  19784  ftc1a  19790  ftc1lem4  19792  ftc1lem6  19794  itgsubstlem  19801  mdegleb  19856  mdegmullem  19870  deg1lt0  19883  ply1divmo  19927  ply1divex  19928  ply1divalg2  19930  q1peqb  19946  fta1g  19959  dgrub  20022  coe1termlem  20045  dgrcolem2  20061  dgrco  20062  quotval  20078  plydivlem3  20081  plydivlem4  20082  plydivex  20083  plydivalg  20085  quotlem  20086  plyrem  20091  fta1  20094  aannenlem1  20114  aannenlem2  20115  aalioulem3  20120  aalioulem4  20121  aalioulem5  20122  aalioulem6  20123  aaliou  20124  aaliou2  20126  aaliou2b  20127  ulmval  20165  ulm2  20170  ulmclm  20172  ulmshftlem  20174  ulmcaulem  20179  ulmcau  20180  ulmss  20182  ulmcn  20184  ulmdvlem1  20185  ulmdvlem3  20187  mtestbdd  20190  iblulm  20192  itgulm  20193  radcnvlem1  20198  pserulm  20207  abelthlem2  20217  abelthlem5  20220  abelthlem7  20223  abelthlem8  20224  abelthlem9  20225  abelth  20226  pilem3  20238  sincosq2sgn  20276  sincosq3sgn  20277  sincosq4sgn  20278  logltb  20363  logcnlem5  20406  cxpcn3lem  20500  cxpcn3  20501  cxpaddle  20505  logreclem  20529  rlimcnp  20673  rlimcnp2  20674  xrlimcnp  20676  rlimcxp  20681  cxploglim  20685  jensen  20696  emcllem6  20708  emcllem7  20709  ftalem2  20725  ftalem3  20726  ftalem5  20728  sqfpc  20789  mumullem2  20832  sqff1o  20834  chtublem  20864  chtub  20865  fsumvma2  20867  chpchtsum  20872  logexprlim  20878  bposlem6  20942  lgslem2  20950  lgslem3  20951  lgsval  20953  lgsfcl2  20955  lgsfle1  20958  lgsle1  20964  lgsdirprm  20982  chtppilimlem2  21037  chtppilim  21038  dchrisumlema  21051  dchrisumlem1  21052  dchrisumlem2  21053  dchrisumlem3  21054  dchrisum  21055  dchrmusumlema  21056  dchrvmasumlem2  21061  dchrisum0flblem1  21071  dchrisum0lema  21077  2vmadivsumlem  21103  chpdifbndlem1  21116  selberg3lem1  21120  selberg4lem1  21123  pntrsumbnd  21129  pntrsumbnd2  21130  selbergsb  21138  pntrlog2bndlem3  21142  pntrlog2bndlem5  21144  pntrlog2bndlem6  21146  pntpbnd1  21149  pntpbnd2  21150  pntibndlem2  21154  pntibndlem3  21155  pntibnd  21156  pntlemn  21163  pntlemj  21166  pntlemi  21167  pntlemo  21170  pntlem3  21172  pntlemp  21173  pntleml  21174  pnt3  21175  padicabv  21193  ostth2lem2  21197  ostth3  21201  ostth  21202  umgrale  21225  umgrafi  21226  umgra1  21230  uslgra1  21261  1pthoncl  21442  2pthoncl  21453  umgrabi  21555  isnvlem  21939  nvelbl  22035  nvelbl2  22036  nmoofval  22113  nmosetn0  22116  nmoolb  22122  nmoubi  22123  nmounbseqi  22128  nmounbseqiOLD  22129  nmobndseqi  22130  nmobndseqiOLD  22131  bloval  22132  isblo  22133  nmoo0  22142  nmlno0lem  22144  blocnilem  22155  siilem2  22203  ubthlem1  22222  ubthlem2  22223  ubthlem3  22224  ubth  22225  minvecolem3  22228  minvecolem4  22232  minvecolem5  22233  minvecolem7  22235  htthlem  22270  htth  22271  h2hcau  22332  h2hlm  22333  normlem7tALT  22471  norm3lemt  22504  hcau  22536  hlimi  22540  hlim2  22544  cmcm3  22967  pjnorm  23076  pjnel  23078  elcnop  23210  elbdop  23213  nmopsetn0  23218  nmfnsetn0  23231  elcnfn  23235  hhcno  23257  hhcnf  23258  nmoplb  23260  nmopub  23261  cnopc  23266  nmfnlb  23277  nmfnleub  23278  cnfnc  23283  idcnop  23334  nmop0  23339  nmfn0  23340  nmlnop0iALT  23348  nmcexi  23379  nmcopexi  23380  lnconi  23386  lnopcon  23388  nmcfnexi  23404  lnfncon  23409  branmfn  23458  leop3  23478  opsqrlem6  23498  cvmd  23689  cvdmd  23690  cvexch  23727  cdj3i  23794  fmptcof2  23920  xraddge02  23961  xdivpnfrp  24020  isofld  24063  ofldadd  24066  ofldmul  24067  sqsscirc2  24113  cnre2csqlem  24114  xrge0iifiso  24127  lmdvg  24144  qqhcn  24176  qqhucn  24177  brfae  24395  dya2ub  24416  ballotlemfc0  24531  ballotlemfcc  24532  ballotlemimin  24544  ballotlemic  24545  ballotlemsv  24548  ballotlemfrcn0  24568  ballotlemrc  24569  lgamgulmlem2  24595  lgamgulmlem3  24596  lgamgulmlem5  24598  lgamgulmlem6  24599  lgambdd  24602  lgamucov  24603  lgamcvglem  24605  erdszelem8  24665  kur14  24683  snmlval  24799  snmlflim  24800  sinccvg  24891  abs2sqle  24901  abs2sqlt  24902  ntrivcvg  25006  ntrivcvgn0  25007  ntrivcvgmullem  25010  prodeq1f  25015  prodeq2w  25019  prodeq2ii  25020  prodrblem2  25038  prodmolem2  25042  prodmo  25043  zprod  25044  fprodntriv  25049  faclim2  25127  poseq  25279  soseq  25280  sltval  25327  brimg  25502  brbtwn2  25560  colinearalg  25565  axcontlem10  25628  cgrtriv  25652  cgrdegen  25654  brofs  25655  cgrextend  25658  segconeu  25661  fvtransport  25682  transportprops  25684  brifs  25693  ifscgr  25694  brcgr3  25696  cgrxfr  25705  brfs  25729  btwnconn1lem7  25743  btwnconn1lem11  25747  btwnconn1lem12  25748  btwnconn1lem14  25750  brsegle  25758  segleantisym  25765  outsideofeu  25781  nndivlub  25924  itg2addnclem  25959  itg2addnc  25961  itg2gt0cn  25962  bddiblnc  25977  ftc1cnnclem  25980  ftc1cnnc  25981  areacirclem2  25984  areacirclem3  25985  areacirclem4  25986  areacirclem5  25988  areacirclem6  25989  areacirc  25990  nn0prpwlem  26018  nn0prpw  26019  seqpo  26144  incsequz2  26146  lmclim2  26157  geomcau  26158  caushft  26160  prdsbnd  26195  ismtyima  26205  heiborlem4  26216  heiborlem6  26218  heiborlem7  26219  bfplem1  26224  bfplem2  26225  rrndstprj2  26233  rrncmslem  26234  rrnequiv  26237  irrapxlem3  26580  irrapxlem4  26581  irrapxlem5  26582  irrapxlem6  26583  pellexlem3  26587  monotoddzz  26699  jm2.19  26757  rmydioph  26778  fnwe2lem2  26819  islinds  26950  lindsss  26965  hbtlem1  26998  hbtlem2  26999  hbtlem7  27000  hbtlem4  27001  hbtlem5  27003  hbtlem6  27004  dgrsub2  27010  symggen  27082  fiuneneq  27184  evth2f  27356  evthf  27368  cncmpmax  27373  rfcnpre4  27375  fmul01  27380  climinf  27402  climsuse  27404  stoweidlem7  27426  stoweidlem9  27428  stoweidlem15  27434  stoweidlem16  27435  stoweidlem18  27437  stoweidlem21  27440  stoweidlem26  27445  stoweidlem31  27450  stoweidlem34  27453  stoweidlem36  27455  stoweidlem37  27456  stoweidlem41  27460  stoweidlem44  27463  stoweidlem45  27464  stoweidlem46  27465  stoweidlem48  27467  stoweidlem51  27470  stoweidlem52  27471  stoweidlem55  27474  stoweidlem59  27478  stoweidlem60  27479  frgrawopreglem2  27799  oposlem  29300  opltcon2b  29323  pats  29402  ishlat1  29469  cvrexch  29536  atle  29552  athgt  29572  1cvrco  29588  3atlem5  29603  4atlem3  29712  dalawlem15  30001  lhprelat3N  30156  lautle  30200  lautcvr  30208  ltrnatb  30253  ltrneq2  30264  cdlemefr32sn2aw  30520  cdlemefs32sn1aw  30530  cdleme32fvaw  30555  cdleme35sn3a  30575  cdleme46frvlpq  30620  cdleme48gfv  30653  trlord  30685  cdlemg1fvawlemN  30689  cdlemg7fvbwN  30723  cdlemg31d  30816  istendo  30876  dva1dim  31101  dvhb1dimN  31102  diafval  31148  diaelval  31150  cdlemm10N  31235  dihopelvalcpre  31365  dihmeetcN  31419  dihmeetlem6  31426  dihjatc1  31428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156
  Copyright terms: Public domain W3C validator