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

Theorem breq1d 4297
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 4290 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  eqbrtrd  4307  syl6eqbr  4324  sbcbr2g  4343  pofun  4652  dffv2  5759  fmptco  5871  isorel  6012  soisores  6013  soisoi  6014  isocnv  6016  isotr  6022  f1owe  6039  weniso  6040  caovordig  6263  caovordg  6265  caovord  6269  f1oweALT  6556  frxp  6677  xporderlem  6678  fnwelem  6682  reldmtpos  6748  brtpos  6749  tpostpos  6760  tposoprab  6776  th3qlem2  7199  ensn1g  7366  fndmeng  7378  xpsneng  7388  xpcomco  7393  pwdom  7455  ordtypelem6  7729  ordtypelem7  7730  wdompwdom  7785  infdiffi  7855  r1sdom  7973  pm54.43  8162  prdom2  8165  indcardi  8203  alephordi  8236  cdalepw  8357  fin23lem26  8486  fin23lem23  8487  fin23lem22  8488  fin23lem27  8489  uniimadomf  8701  alephval2  8728  inar1  8934  nqereu  9090  ltrnq  9140  prlem934  9194  prlem936  9208  ltasr  9259  addgt0sr  9263  axpre-ltadd  9326  axpre-sup  9328  ltsubadd  9801  lesubadd  9803  ltaddsub2  9806  leaddsub2  9808  ltaddpos  9821  lesub2  9826  ltnegcon2  9833  lenegcon2  9836  addge01  9841  subge0  9844  suble0  9845  lesub0  9848  ltordlem  9857  mulgt1  10180  ltmulgt11  10181  gt0div  10187  ge0div  10188  ltmuldiv  10194  ltmuldiv2  10195  lemuldiv2  10204  ltrec  10205  lerec2  10212  ltdiv23  10215  lediv23  10216  addltmul  10552  avglt1  10554  avgle1  10556  avgle  10558  zlem1lt  10688  zgt0ge1  10690  rpnnen1lem5  10975  reexALT  10977  xrmin2  11142  xltnegi  11178  xmulval  11187  xlesubadd  11218  xmullem2  11220  dfceil2  11672  uzenom  11779  seqf1olem1  11837  leexp2r  11913  sqlecan  11964  expmulnbnd  11988  hashbnd  12101  hashle00  12150  hashgt12el2  12166  hashge3el3dif  12179  hashf1  12202  seqcoll  12208  lswccatn0lsw  12279  swrdccatin2  12370  swrd2lsw  12544  2swrd2eqwrdeq  12545  shftfval  12551  shftfib  12553  shftfn  12554  2shfti  12561  shftidt2  12562  sqrlem1  12724  sqrlem2  12725  sqrlem6  12729  sqrlem7  12730  absdiflt  12797  absdifle  12798  lenegsq  12800  cau3lem  12834  limsupgle  12947  limsupgre  12951  clim  12964  rlim  12965  rlim2  12966  clim2  12974  clim0  12976  clim0c  12977  rlim0  12978  rlim0lt  12979  climi0  12982  ello1  12985  ello1mpt  12991  elo1  12996  lo1o1  13002  rlimclim1  13015  rlimclim  13016  climrlim2  13017  rlimuni  13020  climuni  13022  lo1res  13029  rlimresb  13035  rlimeq  13039  2clim  13042  climshftlem  13044  climshft  13046  climabs0  13055  o1co  13056  rlimcn1  13058  rlimcn2  13060  climcn1  13061  climcn2  13062  addcn2  13063  subcn2  13064  mulcn2  13065  o1of2  13082  o1rlimmul  13088  rlimdiv  13115  rlimno1  13123  isershft  13133  isercoll  13137  climsup  13139  climcau  13140  caucvgrlem  13142  caucvgrlem2  13144  caurcvg2  13147  caucvg  13148  caucvgb  13149  serf0  13150  iseraltlem2  13152  iseralt  13154  sumeq1  13158  sumeq2w  13161  sumeq2ii  13162  sumrb  13182  summolem2  13185  summo  13186  zsum  13187  o1fsum  13268  cvgcmp  13271  cvgcmpce  13273  isumshft  13294  climcndslem1  13304  geolim  13322  geolim2  13323  geoisum1c  13332  mertenslem1  13336  mertenslem2  13337  mertens  13338  sin01bnd  13461  cos01bnd  13462  rpnnen  13501  ruclem9  13512  ruclem12  13515  sadcaddlem  13645  gcddvds  13691  dvdssq  13736  isprm  13757  isprm2lem  13762  prmgt1  13774  isprm6  13787  isprm5  13790  odzdvds  13859  pclem  13897  pcprecl  13898  pcprendvds  13899  pcpremul  13902  pcval  13903  pceulem  13904  pczndvds  13923  pcelnn  13928  pc2dvds  13937  pcadd  13943  pcadd2  13944  pcmpt  13946  prmpwdvds  13957  prmreclem1  13969  prmreclem5  13973  prmreclem6  13974  4sqlem17  14014  vdwlem10  14043  ramval  14061  0ram  14073  ram0  14075  ramz2  14077  ramub1lem2  14080  imasaddfnlem  14458  imasvscafn  14467  imasleval  14471  mreexexlemd  14574  symggen  15967  oddvdsnn0  16038  oddvds  16041  odf1  16054  odf1o1  16062  odf1o2  16063  gexdvds  16074  sylow1lem3  16090  efginvrel2  16215  efgsfo  16227  efgredlemd  16232  efgredlem  16235  efgred  16236  gexexlem  16325  torsubg  16327  oddvdssubg  16328  lt6abl  16362  ablfacrplem  16554  ablfacrp  16555  ablfaclem3  16576  abvfval  16881  abvpropd  16905  evlslem2  17572  znf1o  17959  znidomb  17969  cygznlem1  17974  frlmup1  18201  islinds  18213  lindsss  18228  cctop  18585  ordthmeolem  19349  csdfil  19442  ufilen  19478  ptcmplem2  19600  ptcmplem3  19601  cnextfvval  19612  prdsxmetlem  19918  blfvalps  19933  elblps  19937  elbl  19938  elbl3ps  19941  elbl3  19942  blres  19981  imasf1obl  20038  blcld  20055  comet  20063  stdbdmetval  20064  stdbdbl  20067  metcnp2  20092  txmetcnp  20097  dscopn  20141  ngptgp  20197  nlmvscn  20243  nrginvrcn  20247  nmoval  20269  nghmcn  20299  cnbl0  20328  cnblcld  20329  bl2ioo  20344  recld2  20366  icccmplem2  20375  addcnlem  20415  divcn  20419  elcncf  20440  elcncf2  20441  cncfi  20445  rescncf  20448  mulc1cncf  20456  cncfco  20458  cncfmet  20459  cnheiborlem  20501  cnheibor  20502  cnllycmp  20503  evth  20506  htpycc  20527  phtpycc  20538  pcohtpylem  20566  pcoass  20571  pcorevlem  20573  nmoleub2lem2  20646  nmoleub3  20649  nmhmcn  20650  ipcau2  20724  ipcn  20733  lmmbr2  20745  lmmcvg  20747  lmmbrf  20748  fmcfil  20758  iscau2  20763  iscau4  20765  iscauf  20766  caucfil  20769  iscmet3lem3  20776  iscmet3lem1  20777  iscmet3lem2  20778  cfilresi  20781  cfilres  20782  caussi  20783  causs  20784  lmle  20787  lmclim  20788  bcthlem1  20810  bcthlem4  20813  bcth  20815  minveclem3b  20890  minveclem3  20891  minveclem4  20894  minveclem5  20895  minveclem7  20897  pmltpclem1  20907  pmltpc  20909  ivthlem1  20910  ivthlem2  20911  ivthlem3  20912  ivth  20913  cniccbdd  20920  ovolunlem1  20955  ovoliunlem1  20960  ovoliunlem2  20961  ovoliunlem3  20962  ovolshftlem1  20967  ovolscalem1  20971  ovolicc1  20974  ovolicc2lem3  20977  ovolicc2lem4  20978  ovolicc2lem5  20979  ioombl1lem4  21017  ioombl1  21018  uniioombllem6  21043  volsup2  21060  volcn  21061  mbfmulc2lem  21100  mbfsup  21117  mbflimsup  21119  itg1climres  21167  mbfi1fseqlem6  21173  mbfi1fseq  21174  mbfi1flimlem  21175  itg2leub  21187  itg2seq  21195  itg2mulclem  21199  itg2monolem1  21203  itg2mono  21206  itg2i1fseq  21208  itg2addlem  21211  itg2gt0  21213  itg2cnlem1  21214  itg2cnlem2  21215  itg2cn  21216  bddmulibl  21291  itgcn  21295  ellimc3  21329  dveflem  21426  dvferm1lem  21431  dvferm2lem  21433  rolle  21437  dvlip  21440  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  c1lip3  21446  dvge0  21453  dvivthlem1  21455  lhop1lem  21460  lhop1  21461  dvcvx  21467  dvfsumabs  21470  dvfsumlem2  21474  dvfsumrlim  21478  ftc1a  21484  ftc1lem4  21486  ftc1lem6  21488  itgsubstlem  21495  mdegleb  21510  mdegmullem  21524  deg1lt0  21537  ply1divmo  21582  ply1divex  21583  ply1divalg2  21585  q1peqb  21601  fta1g  21614  dgrub  21677  coe1termlem  21700  dgrcolem2  21716  dgrco  21717  quotval  21733  plydivlem3  21736  plydivlem4  21737  plydivex  21738  plydivalg  21740  quotlem  21741  plyrem  21746  fta1  21749  aannenlem1  21769  aannenlem2  21770  aalioulem3  21775  aalioulem4  21776  aalioulem5  21777  aalioulem6  21778  aaliou  21779  aaliou2  21781  aaliou2b  21782  ulmval  21820  ulm2  21825  ulmclm  21827  ulmshftlem  21829  ulmcaulem  21834  ulmcau  21835  ulmss  21837  ulmcn  21839  ulmdvlem1  21840  ulmdvlem3  21842  mtestbdd  21845  iblulm  21847  itgulm  21848  radcnvlem1  21853  pserulm  21862  abelthlem2  21872  abelthlem5  21875  abelthlem7  21878  abelthlem8  21879  abelthlem9  21880  abelth  21881  pilem3  21893  sincosq2sgn  21936  sincosq3sgn  21937  sincosq4sgn  21938  logltb  22023  logcnlem5  22066  cxpcn3lem  22160  cxpcn3  22161  cxpaddle  22165  logreclem  22189  rlimcnp  22334  rlimcnp2  22335  xrlimcnp  22337  rlimcxp  22342  cxploglim  22346  jensen  22357  emcllem6  22369  emcllem7  22370  ftalem2  22386  ftalem3  22387  ftalem5  22389  sqfpc  22450  mumullem2  22493  sqff1o  22495  chtublem  22525  chtub  22526  fsumvma2  22528  chpchtsum  22533  logexprlim  22539  bposlem6  22603  lgslem2  22611  lgslem3  22612  lgsval  22614  lgsfcl2  22616  lgsfle1  22619  lgsle1  22625  lgsdirprm  22643  chtppilimlem2  22698  chtppilim  22699  dchrisumlema  22712  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  dchrisum  22716  dchrmusumlema  22717  dchrvmasumlem2  22722  dchrisum0flblem1  22732  dchrisum0lema  22738  2vmadivsumlem  22764  chpdifbndlem1  22777  selberg3lem1  22781  selberg4lem1  22784  pntrsumbnd  22790  pntrsumbnd2  22791  selbergsb  22799  pntrlog2bndlem3  22803  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntibndlem3  22816  pntibnd  22817  pntlemn  22824  pntlemj  22827  pntlemi  22828  pntlemo  22831  pntlem3  22833  pntlemp  22834  pntleml  22835  pnt3  22836  padicabv  22854  ostth2lem2  22858  ostth3  22862  ostth  22863  nehash2  22935  brbtwn2  23102  colinearalg  23107  axcontlem10  23170  umgrale  23206  umgrafi  23207  umgra1  23211  uslgra1  23242  1pthoncl  23442  2pthoncl  23453  umgrabi  23555  isnvlem  23939  nvelbl  24035  nvelbl2  24036  nmoofval  24113  nmosetn0  24116  nmoolb  24122  nmoubi  24123  nmounbseqi  24128  nmounbseqiOLD  24129  nmobndseqi  24130  nmobndseqiOLD  24131  bloval  24132  isblo  24133  nmoo0  24142  nmlno0lem  24144  blocnilem  24155  siilem2  24203  ubthlem1  24222  ubthlem2  24223  ubthlem3  24224  ubth  24225  minvecolem3  24228  minvecolem4  24232  minvecolem5  24233  minvecolem7  24235  htthlem  24270  htth  24271  h2hcau  24332  h2hlm  24333  normlem7tALT  24472  norm3lemt  24505  hcau  24537  hlimi  24541  hlim2  24545  cmcm3  24969  pjnorm  25078  pjnel  25080  elcnop  25212  elbdop  25215  nmopsetn0  25220  nmfnsetn0  25233  elcnfn  25237  hhcno  25259  hhcnf  25260  nmoplb  25262  nmopub  25263  cnopc  25268  nmfnlb  25279  nmfnleub  25280  cnfnc  25285  idcnop  25336  nmop0  25341  nmfn0  25342  nmlnop0iALT  25350  nmcexi  25381  nmcopexi  25382  lnconi  25388  lnopcon  25390  nmcfnexi  25406  lnfncon  25411  branmfn  25460  leop3  25480  opsqrlem6  25500  cvmd  25691  cvdmd  25692  cvexch  25729  cdj3i  25796  fmptcof2  25930  xraddge02  26001  xdivpnfrp  26059  omndadd  26120  omndmul  26128  archirngz  26157  archiabllem2a  26162  isorng  26218  sqsscirc2  26291  cnre2csqlem  26292  xrge0iifiso  26317  lmdvg  26335  qqhcn  26372  qqhucn  26373  brfae  26616  dya2ub  26637  oddpwdc  26689  eulerpartlemd  26701  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemimin  26840  ballotlemic  26841  ballotlemsv  26844  ballotlemfrcn0  26864  ballotlemrc  26865  sgnmul  26877  sgnmulsgn  26884  signsplypnf  26903  signsply0  26904  signswch  26914  signsvfn  26935  signsvfnn  26939  signlem0  26940  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem5  26971  lgamgulmlem6  26972  lgambdd  26975  lgamucov  26976  lgamcvglem  26978  erdszelem8  27038  kur14  27056  snmlval  27172  snmlflim  27173  sinccvg  27269  abs2sqle  27276  abs2sqlt  27277  ntrivcvg  27363  ntrivcvgn0  27364  ntrivcvgmullem  27367  prodeq1f  27372  prodeq2w  27376  prodeq2ii  27377  prodrblem2  27395  prodmolem2  27399  prodmo  27400  zprod  27401  fprodntriv  27406  faclim2  27505  poseq  27665  soseq  27666  sltval  27739  brimg  27919  cgrtriv  27984  cgrdegen  27986  brofs  27987  cgrextend  27990  segconeu  27993  fvtransport  28014  transportprops  28016  brifs  28025  ifscgr  28026  brcgr3  28028  cgrxfr  28037  brfs  28061  btwnconn1lem7  28075  btwnconn1lem11  28079  btwnconn1lem12  28080  btwnconn1lem14  28082  brsegle  28090  segleantisym  28097  outsideofeu  28113  nndivlub  28256  heicant  28379  dvtanlem  28394  itg2addnclem  28396  itg2addnclem3  28398  itg2addnc  28399  itg2gt0cn  28400  bddiblnc  28415  ftc1cnnclem  28418  ftc1cnnc  28419  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anc  28428  areacirclem1  28437  areacirclem2  28438  areacirclem4  28440  areacirclem5  28441  areacirc  28442  nn0prpwlem  28470  nn0prpw  28471  seqpo  28596  incsequz2  28598  lmclim2  28607  geomcau  28608  caushft  28610  prdsbnd  28645  ismtyima  28655  heiborlem4  28666  heiborlem6  28668  heiborlem7  28669  bfplem1  28674  bfplem2  28675  rrndstprj2  28683  rrncmslem  28684  rrnequiv  28687  irrapxlem3  29118  irrapxlem4  29119  irrapxlem5  29120  irrapxlem6  29121  pellexlem3  29125  monotoddzz  29237  jm2.19  29295  rmydioph  29316  fnwe2lem2  29357  hbtlem1  29432  hbtlem2  29433  hbtlem7  29434  hbtlem4  29435  hbtlem5  29437  hbtlem6  29438  dgrsub2  29444  fiuneneq  29515  evth2f  29690  evthf  29702  cncmpmax  29707  rfcnpre4  29709  fmul01  29714  climinf  29732  climsuse  29734  stoweidlem7  29755  stoweidlem9  29757  stoweidlem15  29763  stoweidlem16  29764  stoweidlem18  29766  stoweidlem21  29769  stoweidlem26  29774  stoweidlem31  29779  stoweidlem34  29782  stoweidlem36  29784  stoweidlem37  29785  stoweidlem41  29789  stoweidlem44  29792  stoweidlem45  29793  stoweidlem46  29794  stoweidlem48  29796  stoweidlem51  29799  stoweidlem52  29800  stoweidlem55  29803  stoweidlem59  29807  stoweidlem60  29808  prmn2uzge3  30202  clwlkisclwwlk2  30405  0eusgraiff0rgra  30505  frgrawopreglem2  30591  snnen2o  30690  supgtoreq  30694  pgrpgt2nabel  30720  oposlem  32667  opltcon2b  32691  pats  32770  ishlat1  32837  cvrexch  32904  atle  32920  athgt  32940  1cvrco  32956  3atlem5  32971  4atlem3  33080  dalawlem15  33369  lhprelat3N  33524  lautle  33568  lautcvr  33576  ltrnatb  33621  ltrneq2  33632  cdlemefr32sn2aw  33888  cdlemefs32sn1aw  33898  cdleme32fvaw  33923  cdleme35sn3a  33943  cdleme46frvlpq  33988  cdleme48gfv  34021  trlord  34053  cdlemg1fvawlemN  34057  cdlemg7fvbwN  34091  cdlemg31d  34184  istendo  34244  dva1dim  34469  dvhb1dimN  34470  diafval  34516  diaelval  34518  cdlemm10N  34603  dihopelvalcpre  34733  dihmeetcN  34787  dihmeetlem6  34794  dihjatc1  34796
  Copyright terms: Public domain W3C validator