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

Theorem breq1d 4163
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 4156 . 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 4153
This theorem is referenced by:  eqbrtrd  4173  syl6eqbr  4190  sbcbr2g  4205  pofun  4460  dffv2  5735  fmptco  5840  isorel  5985  soisores  5986  soisoi  5987  isocnv  5989  isotr  5995  f1owe  6012  f1oweALT  6013  weniso  6014  caovordig  6191  caovordg  6193  caovord  6197  frxp  6392  xporderlem  6393  fnwelem  6397  reldmtpos  6423  brtpos  6424  tpostpos  6435  tposoprab  6451  th3qlem2  6947  ensn1g  7108  fndmeng  7119  xpsneng  7129  xpcomco  7134  pwdom  7195  ordtypelem6  7425  ordtypelem7  7426  wdompwdom  7479  infdiffi  7545  r1sdom  7633  pm54.43  7820  prdom2  7823  indcardi  7855  alephordi  7888  cdalepw  8009  fin23lem26  8138  fin23lem23  8139  fin23lem22  8140  fin23lem27  8141  uniimadomf  8353  alephval2  8380  inar1  8583  nqereu  8739  ltrnq  8789  prlem934  8843  prlem936  8857  ltasr  8908  addgt0sr  8912  axpre-ltadd  8975  axpre-sup  8977  ltsubadd  9430  lesubadd  9432  ltaddsub2  9435  leaddsub2  9437  ltaddpos  9450  lesub2  9455  ltnegcon2  9462  lenegcon2  9465  addge01  9470  subge0  9473  suble0  9474  lesub0  9476  ltordlem  9484  mulgt1  9801  ltmulgt11  9802  gt0div  9808  ge0div  9809  ltmuldiv  9812  ltmuldiv2  9813  lemuldiv2  9822  ltrec  9823  lerec2  9830  ltdiv23  9833  lediv23  9834  addltmul  10135  avglt1  10137  avgle1  10139  avgle  10141  zlem1lt  10259  rpnnen1lem5  10536  reexALT  10538  xrmin2  10698  xltnegi  10734  xmulval  10743  xlesubadd  10774  xmullem2  10776  uzenom  11231  seqf1olem1  11289  leexp2r  11364  sqlecan  11414  expmulnbnd  11438  hashbnd  11551  hashle00  11596  hashgt12el2  11610  hashf1  11633  seqcoll  11639  shftfval  11812  shftfib  11814  shftfn  11815  2shfti  11822  shftidt2  11823  sqrlem1  11975  sqrlem2  11976  sqrlem6  11980  sqrlem7  11981  absdiflt  12048  absdifle  12049  lenegsq  12051  cau3lem  12085  limsupgle  12198  limsupgre  12202  clim  12215  rlim  12216  rlim2  12217  clim2  12225  clim0  12227  clim0c  12228  rlim0  12229  rlim0lt  12230  climi0  12233  ello1  12236  ello1mpt  12242  elo1  12247  lo1o1  12253  rlimclim1  12266  rlimclim  12267  climrlim2  12268  rlimuni  12271  climuni  12273  lo1res  12280  rlimresb  12286  rlimeq  12290  2clim  12293  climshftlem  12295  climshft  12297  climabs0  12306  o1co  12307  rlimcn1  12309  rlimcn2  12311  climcn1  12312  climcn2  12313  addcn2  12314  subcn2  12315  mulcn2  12316  o1of2  12333  o1rlimmul  12339  rlimdiv  12366  rlimno1  12374  isershft  12384  isercoll  12388  climsup  12390  climcau  12391  caucvgrlem  12393  caucvgrlem2  12395  caurcvg2  12398  caucvg  12399  caucvgb  12400  serf0  12401  iseraltlem2  12403  iseralt  12405  sumeq1f  12409  sumeq2w  12413  sumeq2ii  12414  cbvsum  12416  sumrb  12434  summolem2  12437  summo  12438  zsum  12439  o1fsum  12519  cvgcmp  12522  cvgcmpce  12524  isumshft  12546  climcndslem1  12556  geolim  12574  geolim2  12575  geoisum1c  12584  mertenslem1  12588  mertenslem2  12589  mertens  12590  sin01bnd  12713  cos01bnd  12714  rpnnen  12753  ruclem9  12764  ruclem12  12767  sadcaddlem  12896  gcddvds  12942  dvdssq  12987  isprm  13008  isprm2lem  13013  isprm6  13036  isprm5  13039  odzdvds  13108  pclem  13139  pcprecl  13140  pcprendvds  13141  pcpremul  13144  pcval  13145  pceulem  13146  pczndvds  13165  pcelnn  13170  pc2dvds  13179  pcadd  13185  pcadd2  13186  pcmpt  13188  prmpwdvds  13199  prmreclem1  13211  prmreclem5  13215  prmreclem6  13216  4sqlem17  13256  vdwlem10  13285  ramval  13303  0ram  13315  ram0  13317  ramz2  13319  ramub1lem2  13322  imasaddfnlem  13680  imasvscafn  13689  imasleval  13693  mreexexlemd  13796  oddvdsnn0  15109  oddvds  15112  odf1  15125  odf1o1  15133  odf1o2  15134  gexdvds  15145  sylow1lem3  15161  efginvrel2  15286  efgsfo  15298  efgredlemd  15303  efgredlem  15306  efgred  15307  gexexlem  15394  torsubg  15396  oddvdssubg  15397  lt6abl  15431  ablfacrplem  15550  ablfacrp  15551  ablfaclem3  15572  abvfval  15833  abvpropd  15857  znf1o  16755  znidomb  16765  cygznlem1  16770  cctop  16993  ordthmeolem  17754  csdfil  17847  ufilen  17883  ptcmplem2  18005  ptcmplem3  18006  cnextfvval  18017  prdsxmetlem  18306  blfval  18321  elbl  18323  elbl3  18325  blres  18351  imasf1obl  18408  blcld  18425  comet  18433  stdbdmetval  18434  stdbdbl  18437  metcnp2  18462  txmetcnp  18467  dscopn  18492  ngptgp  18548  nlmvscn  18594  nrginvrcn  18598  nmoval  18620  nghmcn  18650  cnbl0  18679  cnblcld  18680  bl2ioo  18694  recld2  18716  icccmplem2  18725  addcnlem  18765  divcn  18769  elcncf  18790  elcncf2  18791  cncfi  18795  rescncf  18798  mulc1cncf  18806  cncfco  18808  cncfmet  18809  cnheiborlem  18850  cnheibor  18851  cnllycmp  18852  evth  18855  htpycc  18876  phtpycc  18887  pcohtpylem  18915  pcoass  18920  pcorevlem  18922  nmoleub2lem2  18995  nmoleub3  18998  nmhmcn  18999  ipcau2  19062  ipcn  19071  lmmbr2  19083  lmmcvg  19085  lmmbrf  19086  fmcfil  19096  iscau2  19101  iscau4  19103  iscauf  19104  caucfil  19107  iscmet3lem3  19114  iscmet3lem1  19115  iscmet3lem2  19116  cfilresi  19119  cfilres  19120  caussi  19121  causs  19122  lmle  19125  lmclim  19126  bcthlem1  19146  bcthlem4  19149  bcth  19151  minveclem3b  19196  minveclem3  19197  minveclem4  19200  minveclem5  19201  minveclem7  19203  pmltpclem1  19212  pmltpc  19214  ivthlem1  19215  ivthlem2  19216  ivthlem3  19217  ivth  19218  cniccbdd  19225  ovolunlem1  19260  ovoliunlem1  19265  ovoliunlem2  19266  ovoliunlem3  19267  ovolshftlem1  19272  ovolscalem1  19276  ovolicc1  19279  ovolicc2lem3  19282  ovolicc2lem4  19283  ovolicc2lem5  19284  ioombl1lem4  19322  ioombl1  19323  uniioombllem6  19347  volsup2  19364  volcn  19365  mbfmulc2lem  19406  mbfsup  19423  mbflimsup  19425  itg1climres  19473  mbfi1fseqlem6  19479  mbfi1fseq  19480  mbfi1flimlem  19481  itg2leub  19493  itg2seq  19501  itg2mulclem  19505  itg2monolem1  19509  itg2mono  19512  itg2i1fseq  19514  itg2addlem  19517  itg2gt0  19519  itg2cnlem1  19520  itg2cnlem2  19521  itg2cn  19522  bddmulibl  19597  itgcn  19601  ellimc3  19633  dveflem  19730  dvferm1lem  19735  dvferm2lem  19737  rolle  19741  dvlip  19744  dvlipcn  19745  dvlip2  19746  c1liplem1  19747  c1lip3  19750  dvge0  19757  dvivthlem1  19759  lhop1lem  19764  lhop1  19765  dvcvx  19771  dvfsumabs  19774  dvfsumlem2  19778  dvfsumrlim  19782  ftc1a  19788  ftc1lem4  19790  ftc1lem6  19792  itgsubstlem  19799  mdegleb  19854  mdegmullem  19868  deg1lt0  19881  ply1divmo  19925  ply1divex  19926  ply1divalg2  19928  q1peqb  19944  fta1g  19957  dgrub  20020  coe1termlem  20043  dgrcolem2  20059  dgrco  20060  quotval  20076  plydivlem3  20079  plydivlem4  20080  plydivex  20081  plydivalg  20083  quotlem  20084  plyrem  20089  fta1  20092  aannenlem1  20112  aannenlem2  20113  aalioulem3  20118  aalioulem4  20119  aalioulem5  20120  aalioulem6  20121  aaliou  20122  aaliou2  20124  aaliou2b  20125  ulmval  20163  ulm2  20168  ulmclm  20170  ulmshftlem  20172  ulmcaulem  20177  ulmcau  20178  ulmss  20180  ulmcn  20182  ulmdvlem1  20183  ulmdvlem3  20185  mtestbdd  20188  iblulm  20190  itgulm  20191  radcnvlem1  20196  pserulm  20205  abelthlem2  20215  abelthlem5  20218  abelthlem7  20221  abelthlem8  20222  abelthlem9  20223  abelth  20224  pilem3  20236  sincosq2sgn  20274  sincosq3sgn  20275  sincosq4sgn  20276  logltb  20361  logcnlem5  20404  cxpcn3lem  20498  cxpcn3  20499  cxpaddle  20503  logreclem  20527  rlimcnp  20671  rlimcnp2  20672  xrlimcnp  20674  rlimcxp  20679  cxploglim  20683  jensen  20694  emcllem6  20706  emcllem7  20707  ftalem2  20723  ftalem3  20724  ftalem5  20726  sqfpc  20787  mumullem2  20830  sqff1o  20832  chtublem  20862  chtub  20863  fsumvma2  20865  chpchtsum  20870  logexprlim  20876  bposlem6  20940  lgslem2  20948  lgslem3  20949  lgsval  20951  lgsfcl2  20953  lgsfle1  20956  lgsle1  20962  lgsdirprm  20980  chtppilimlem2  21035  chtppilim  21036  dchrisumlema  21049  dchrisumlem1  21050  dchrisumlem2  21051  dchrisumlem3  21052  dchrisum  21053  dchrmusumlema  21054  dchrvmasumlem2  21059  dchrisum0flblem1  21069  dchrisum0lema  21075  2vmadivsumlem  21101  chpdifbndlem1  21114  selberg3lem1  21118  selberg4lem1  21121  pntrsumbnd  21127  pntrsumbnd2  21128  selbergsb  21136  pntrlog2bndlem3  21140  pntrlog2bndlem5  21142  pntrlog2bndlem6  21144  pntpbnd1  21147  pntpbnd2  21148  pntibndlem2  21152  pntibndlem3  21153  pntibnd  21154  pntlemn  21161  pntlemj  21164  pntlemi  21165  pntlemo  21168  pntlem3  21170  pntlemp  21171  pntleml  21172  pnt3  21173  padicabv  21191  ostth2lem2  21195  ostth3  21199  ostth  21200  umgrale  21223  umgrafi  21224  umgra1  21228  uslgra1  21259  1pthoncl  21440  2pthoncl  21451  umgrabi  21553  isnvlem  21937  nvelbl  22033  nvelbl2  22034  nmoofval  22111  nmosetn0  22114  nmoolb  22120  nmoubi  22121  nmounbseqi  22126  nmounbseqiOLD  22127  nmobndseqi  22128  nmobndseqiOLD  22129  bloval  22130  isblo  22131  nmoo0  22140  nmlno0lem  22142  blocnilem  22153  siilem2  22201  ubthlem1  22220  ubthlem2  22221  ubthlem3  22222  ubth  22223  minvecolem3  22226  minvecolem4  22230  minvecolem5  22231  minvecolem7  22233  htthlem  22268  htth  22269  h2hcau  22330  h2hlm  22331  normlem7tALT  22469  norm3lemt  22502  hcau  22534  hlimi  22538  hlim2  22542  cmcm3  22965  pjnorm  23074  pjnel  23076  elcnop  23208  elbdop  23211  nmopsetn0  23216  nmfnsetn0  23229  elcnfn  23233  hhcno  23255  hhcnf  23256  nmoplb  23258  nmopub  23259  cnopc  23264  nmfnlb  23275  nmfnleub  23276  cnfnc  23281  idcnop  23332  nmop0  23337  nmfn0  23338  nmlnop0iALT  23346  nmcexi  23377  nmcopexi  23378  lnconi  23384  lnopcon  23386  nmcfnexi  23402  lnfncon  23407  branmfn  23456  leop3  23476  opsqrlem6  23496  cvmd  23687  cvdmd  23688  cvexch  23725  cdj3i  23792  fmptcof2  23918  xraddge02  23959  xdivpnfrp  24018  isofld  24061  ofldadd  24064  ofldmul  24065  sqsscirc2  24111  cnre2csqlem  24112  xrge0iifiso  24125  lmdvg  24142  qqhcn  24174  qqhucn  24175  brfae  24393  dya2ub  24414  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemimin  24542  ballotlemic  24543  ballotlemsv  24546  ballotlemfrcn0  24566  ballotlemrc  24567  lgamgulmlem2  24593  lgamgulmlem3  24594  lgamgulmlem5  24596  lgamgulmlem6  24597  lgambdd  24600  lgamucov  24601  lgamcvglem  24603  erdszelem8  24663  kur14  24681  snmlval  24797  snmlflim  24798  sinccvg  24889  abs2sqle  24899  abs2sqlt  24900  ntrivcvg  25004  ntrivcvgn0  25005  ntrivcvgmullem  25008  prodeq1f  25013  prodeq2w  25017  prodeq2ii  25018  prodrblem2  25036  prodmolem2  25040  prodmo  25041  zprod  25042  fprodntriv  25047  faclim2  25125  poseq  25277  soseq  25278  sltval  25325  brimg  25500  brbtwn2  25558  colinearalg  25563  axcontlem10  25626  cgrtriv  25650  cgrdegen  25652  brofs  25653  cgrextend  25656  segconeu  25659  fvtransport  25680  transportprops  25682  brifs  25691  ifscgr  25692  brcgr3  25694  cgrxfr  25703  brfs  25727  btwnconn1lem7  25741  btwnconn1lem11  25745  btwnconn1lem12  25746  btwnconn1lem14  25748  brsegle  25756  segleantisym  25763  outsideofeu  25779  nndivlub  25922  itg2addnclem  25957  itg2addnc  25959  itg2gt0cn  25960  bddiblnc  25975  ftc1cnnclem  25978  ftc1cnnc  25979  areacirclem2  25982  areacirclem3  25983  areacirclem4  25984  areacirclem5  25986  areacirclem6  25987  areacirc  25988  nn0prpwlem  26016  nn0prpw  26017  seqpo  26142  incsequz2  26144  lmclim2  26155  geomcau  26156  caushft  26158  prdsbnd  26193  ismtyima  26203  heiborlem4  26214  heiborlem6  26216  heiborlem7  26217  bfplem1  26222  bfplem2  26223  rrndstprj2  26231  rrncmslem  26232  rrnequiv  26235  irrapxlem3  26578  irrapxlem4  26579  irrapxlem5  26580  irrapxlem6  26581  pellexlem3  26585  monotoddzz  26697  jm2.19  26755  rmydioph  26776  fnwe2lem2  26817  islinds  26948  lindsss  26963  hbtlem1  26996  hbtlem2  26997  hbtlem7  26998  hbtlem4  26999  hbtlem5  27001  hbtlem6  27002  dgrsub2  27008  symggen  27080  fiuneneq  27182  evth2f  27354  evthf  27366  cncmpmax  27371  rfcnpre4  27373  fmul01  27378  climinf  27400  climsuse  27402  stoweidlem7  27424  stoweidlem9  27426  stoweidlem15  27432  stoweidlem16  27433  stoweidlem18  27435  stoweidlem21  27438  stoweidlem26  27443  stoweidlem31  27448  stoweidlem34  27451  stoweidlem36  27453  stoweidlem37  27454  stoweidlem41  27458  stoweidlem44  27461  stoweidlem45  27462  stoweidlem46  27463  stoweidlem48  27465  stoweidlem51  27468  stoweidlem52  27469  stoweidlem55  27472  stoweidlem59  27476  stoweidlem60  27477  frgrawopreglem2  27797  oposlem  29298  opltcon2b  29321  pats  29400  ishlat1  29467  cvrexch  29534  atle  29550  athgt  29570  1cvrco  29586  3atlem5  29601  4atlem3  29710  dalawlem15  29999  lhprelat3N  30154  lautle  30198  lautcvr  30206  ltrnatb  30251  ltrneq2  30262  cdlemefr32sn2aw  30518  cdlemefs32sn1aw  30528  cdleme32fvaw  30553  cdleme35sn3a  30573  cdleme46frvlpq  30618  cdleme48gfv  30651  trlord  30683  cdlemg1fvawlemN  30687  cdlemg7fvbwN  30721  cdlemg31d  30814  istendo  30874  dva1dim  31099  dvhb1dimN  31100  diafval  31146  diaelval  31148  cdlemm10N  31233  dihopelvalcpre  31363  dihmeetcN  31417  dihmeetlem6  31424  dihjatc1  31426
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 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154
  Copyright terms: Public domain W3C validator