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

Theorem breq1d 4033
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 4026 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 15 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  eqbrtrd  4043  syl6eqbr  4060  sbcbr2g  4075  pofun  4330  dffv2  5592  fmptco  5691  isorel  5823  soisores  5824  soisoi  5825  isocnv  5827  isotr  5833  f1owe  5850  f1oweALT  5851  weniso  5852  caovordig  6025  caovordg  6027  caovord  6031  frxp  6225  xporderlem  6226  fnwelem  6230  reldmtpos  6242  brtpos  6243  tpostpos  6254  tposoprab  6270  th3qlem2  6765  ensn1g  6926  fndmeng  6937  xpsneng  6947  xpcomco  6952  pwdom  7013  ordtypelem6  7238  ordtypelem7  7239  wdompwdom  7292  infdiffi  7358  r1sdom  7446  pm54.43  7633  prdom2  7636  indcardi  7668  alephordi  7701  cdalepw  7822  fin23lem26  7951  fin23lem23  7952  fin23lem22  7953  fin23lem27  7954  uniimadomf  8167  alephval2  8194  inar1  8397  nqereu  8553  ltrnq  8603  prlem934  8657  prlem936  8671  ltasr  8722  addgt0sr  8726  axpre-ltadd  8789  axpre-sup  8791  ltsubadd  9244  lesubadd  9246  ltaddsub2  9249  leaddsub2  9251  ltaddpos  9264  lesub2  9269  ltnegcon2  9276  lenegcon2  9279  addge01  9284  subge0  9287  suble0  9288  lesub0  9290  ltordlem  9298  mulgt1  9615  ltmulgt11  9616  gt0div  9622  ge0div  9623  ltmuldiv  9626  ltmuldiv2  9627  lemuldiv2  9636  ltrec  9637  lerec2  9644  ltdiv23  9647  lediv23  9648  addltmul  9947  avglt1  9949  avgle1  9951  avgle  9953  zlem1lt  10069  rpnnen1lem5  10346  reexALT  10348  xrmin2  10507  xltnegi  10543  xmulval  10552  xlesubadd  10583  xmullem2  10585  uzenom  11027  seqf1olem1  11085  leexp2r  11159  sqlecan  11209  expmulnbnd  11233  hashbnd  11343  hashf1  11395  seqcoll  11401  shftfval  11565  shftfib  11567  shftfn  11568  2shfti  11575  shftidt2  11576  sqrlem1  11728  sqrlem2  11729  sqrlem6  11733  sqrlem7  11734  absdiflt  11801  absdifle  11802  lenegsq  11804  cau3lem  11838  limsupgle  11951  limsupgre  11955  clim  11968  rlim  11969  rlim2  11970  clim2  11978  clim0  11980  clim0c  11981  rlim0  11982  rlim0lt  11983  climi0  11986  ello1  11989  ello1mpt  11995  elo1  12000  lo1o1  12006  rlimclim1  12019  rlimclim  12020  climrlim2  12021  rlimuni  12024  climuni  12026  lo1res  12033  rlimresb  12039  rlimeq  12043  2clim  12046  climshftlem  12048  climshft  12050  climabs0  12059  o1co  12060  rlimcn1  12062  rlimcn2  12064  climcn1  12065  climcn2  12066  addcn2  12067  subcn2  12068  mulcn2  12069  o1of2  12086  o1rlimmul  12092  rlimdiv  12119  rlimno1  12127  isershft  12137  isercoll  12141  climsup  12143  climcau  12144  caucvgrlem  12145  caucvgrlem2  12147  caurcvg2  12150  caucvg  12151  caucvgb  12152  serf0  12153  iseraltlem2  12155  iseralt  12157  sumeq1f  12161  sumeq2w  12165  sumeq2ii  12166  cbvsum  12168  sumrb  12186  summolem2  12189  summo  12190  zsum  12191  o1fsum  12271  cvgcmp  12274  cvgcmpce  12276  isumshft  12298  climcndslem1  12308  geolim  12326  geolim2  12327  geoisum1c  12336  mertenslem1  12340  mertenslem2  12341  mertens  12342  sin01bnd  12465  cos01bnd  12466  rpnnen  12505  ruclem9  12516  ruclem12  12519  sadcaddlem  12648  gcddvds  12694  dvdssq  12739  isprm  12760  isprm2lem  12765  isprm6  12788  isprm5  12791  odzdvds  12860  pclem  12891  pcprecl  12892  pcprendvds  12893  pcpremul  12896  pcval  12897  pceulem  12898  pczndvds  12917  pcelnn  12922  pc2dvds  12931  pcadd  12937  pcadd2  12938  pcmpt  12940  prmpwdvds  12951  prmreclem1  12963  prmreclem5  12967  prmreclem6  12968  4sqlem17  13008  vdwlem10  13037  ramval  13055  0ram  13067  ram0  13069  ramz2  13071  ramub1lem2  13074  imasaddfnlem  13430  imasvscafn  13439  imasleval  13443  mreexexlemd  13546  oddvdsnn0  14859  oddvds  14862  odf1  14875  odf1o1  14883  odf1o2  14884  gexdvds  14895  sylow1lem3  14911  efginvrel2  15036  efgsfo  15048  efgredlemd  15053  efgredlem  15056  efgred  15057  gexexlem  15144  torsubg  15146  oddvdssubg  15147  lt6abl  15181  ablfacrplem  15300  ablfacrp  15301  ablfaclem3  15322  abvfval  15583  abvpropd  15607  znf1o  16505  znidomb  16515  cygznlem1  16520  cctop  16743  ordthmeolem  17492  csdfil  17589  ufilen  17625  ptcmplem2  17747  ptcmplem3  17748  prdsxmetlem  17932  blfval  17947  elbl  17949  elbl3  17951  blres  17977  imasf1obl  18034  blcld  18051  comet  18059  stdbdmetval  18060  stdbdbl  18063  metcnp2  18088  txmetcnp  18093  dscopn  18096  ngptgp  18152  nlmvscn  18198  nrginvrcn  18202  nmoval  18224  nghmcn  18254  cnbl0  18283  cnblcld  18284  bl2ioo  18298  recld2  18320  icccmplem2  18328  addcnlem  18368  divcn  18372  elcncf  18393  elcncf2  18394  cncfi  18398  rescncf  18401  mulc1cncf  18409  cncfco  18411  cncfmet  18412  cnheiborlem  18452  cnheibor  18453  cnllycmp  18454  evth  18457  htpycc  18478  phtpycc  18489  pcohtpylem  18517  pcoass  18522  pcorevlem  18524  nmoleub2lem2  18597  nmoleub3  18600  nmhmcn  18601  ipcau2  18664  ipcn  18673  lmmbr2  18685  lmmcvg  18687  lmmbrf  18688  fmcfil  18698  iscau2  18703  iscau4  18705  iscauf  18706  caucfil  18709  iscmet3lem3  18716  iscmet3lem1  18717  iscmet3lem2  18718  cfilresi  18721  cfilres  18722  caussi  18723  causs  18724  lmle  18727  lmclim  18728  bcthlem1  18746  bcthlem4  18749  bcth  18751  minveclem3b  18792  minveclem3  18793  minveclem4  18796  minveclem5  18797  minveclem7  18799  pmltpclem1  18808  pmltpc  18810  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ivth  18814  cniccbdd  18821  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliunlem3  18863  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ioombl1lem4  18918  ioombl1  18919  uniioombllem6  18943  volsup2  18960  volcn  18961  mbfmulc2lem  19002  mbfsup  19019  mbflimsup  19021  itg1climres  19069  mbfi1fseqlem6  19075  mbfi1fseq  19076  mbfi1flimlem  19077  itg2leub  19089  itg2seq  19097  itg2mulclem  19101  itg2monolem1  19105  itg2mono  19108  itg2i1fseq  19110  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  bddmulibl  19193  itgcn  19197  ellimc3  19229  dveflem  19326  dvferm1lem  19331  dvferm2lem  19333  rolle  19337  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  c1lip3  19346  dvge0  19353  dvivthlem1  19355  lhop1lem  19360  lhop1  19361  dvcvx  19367  dvfsumabs  19370  dvfsumlem2  19374  dvfsumrlim  19378  ftc1a  19384  ftc1lem4  19386  ftc1lem6  19388  itgsubstlem  19395  mdegleb  19450  mdegmullem  19464  deg1lt0  19477  ply1divmo  19521  ply1divex  19522  ply1divalg2  19524  q1peqb  19540  fta1g  19553  dgrub  19616  coe1termlem  19639  dgrcolem2  19655  dgrco  19656  quotval  19672  plydivlem3  19675  plydivlem4  19676  plydivex  19677  plydivalg  19679  quotlem  19680  plyrem  19685  fta1  19688  aannenlem1  19708  aannenlem2  19709  aalioulem3  19714  aalioulem4  19715  aalioulem5  19716  aalioulem6  19717  aaliou  19718  aaliou2  19720  aaliou2b  19721  ulmval  19759  ulm2  19764  ulmclm  19766  ulmshftlem  19768  ulmcaulem  19771  ulmcau  19772  ulmss  19774  ulmcn  19776  ulmdvlem1  19777  ulmdvlem3  19779  iblulm  19783  itgulm  19784  radcnvlem1  19789  pserulm  19798  abelthlem2  19808  abelthlem5  19811  abelthlem7  19814  abelthlem8  19815  abelthlem9  19816  abelth  19817  pilem3  19829  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  logltb  19953  logcnlem5  19993  cxpcn3lem  20087  cxpcn3  20088  cxpaddle  20092  logreclem  20116  rlimcnp  20260  rlimcnp2  20261  xrlimcnp  20263  rlimcxp  20268  cxploglim  20272  jensen  20283  emcllem6  20294  emcllem7  20295  ftalem2  20311  ftalem3  20312  ftalem5  20314  sqfpc  20375  mumullem2  20418  sqff1o  20420  chtublem  20450  chtub  20451  fsumvma2  20453  chpchtsum  20458  logexprlim  20464  bposlem6  20528  lgslem2  20536  lgslem3  20537  lgsval  20539  lgsfcl2  20541  lgsfle1  20544  lgsle1  20550  lgsdirprm  20568  chtppilimlem2  20623  chtppilim  20624  dchrisumlema  20637  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrisum  20641  dchrmusumlema  20642  dchrvmasumlem2  20647  dchrisum0flblem1  20657  dchrisum0lema  20663  2vmadivsumlem  20689  chpdifbndlem1  20702  selberg3lem1  20706  selberg4lem1  20709  pntrsumbnd  20715  pntrsumbnd2  20716  selbergsb  20724  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemn  20749  pntlemj  20752  pntlemi  20753  pntlemo  20756  pntlem3  20758  pntlemp  20759  pntleml  20760  pnt3  20761  padicabv  20779  ostth2lem2  20783  ostth3  20787  ostth  20788  isnvlem  21166  nvelbl  21262  nvelbl2  21263  nmoofval  21340  nmosetn0  21343  nmoolb  21349  nmoubi  21350  nmounbseqi  21355  nmounbseqiOLD  21356  nmobndseqi  21357  nmobndseqiOLD  21358  bloval  21359  isblo  21360  nmoo0  21369  nmlno0lem  21371  blocnilem  21382  siilem2  21430  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  ubth  21452  minvecolem3  21455  minvecolem4  21459  minvecolem5  21460  minvecolem7  21462  htthlem  21497  htth  21498  h2hcau  21559  h2hlm  21560  normlem7tALT  21698  norm3lemt  21731  hcau  21763  hlimi  21767  hlim2  21771  cmcm3  22194  pjnorm  22303  pjnel  22305  elcnop  22437  elbdop  22440  nmopsetn0  22445  nmfnsetn0  22458  elcnfn  22462  hhcno  22484  hhcnf  22485  nmoplb  22487  nmopub  22488  cnopc  22493  nmfnlb  22504  nmfnleub  22505  cnfnc  22510  idcnop  22561  nmop0  22566  nmfn0  22567  nmlnop0iALT  22575  nmcexi  22606  nmcopexi  22607  lnconi  22613  lnopcon  22615  nmcfnexi  22631  lnfncon  22636  branmfn  22685  leop3  22705  opsqrlem6  22725  cvmd  22916  cvdmd  22917  cvexch  22954  cdj3i  23021  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemimin  23064  ballotlemic  23065  ballotlem1c  23066  ballotlemsv  23068  ballotlemfrcn0  23088  ballotlemrc  23089  xdivpnfrp  23117  fmptcof2  23229  xraddge02  23252  sqsscirc2  23293  cnre2csqlem  23294  xrge0iifiso  23317  lmdvg  23376  dya2ub  23575  erdszelem8  23729  kur14  23747  umgrale  23873  umgrafi  23874  umgra1  23878  umgrabi  23907  snmlval  23914  snmlflim  23915  sinccvg  24006  abs2sqle  24016  abs2sqlt  24017  poseq  24253  soseq  24254  sltval  24301  brimg  24476  brbtwn2  24533  colinearalg  24538  axcontlem10  24601  cgrtriv  24625  cgrdegen  24627  brofs  24628  cgrextend  24631  segconeu  24634  fvtransport  24655  transportprops  24657  brifs  24666  ifscgr  24667  brcgr3  24669  cgrxfr  24678  brfs  24702  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem14  24723  brsegle  24731  segleantisym  24738  outsideofeu  24754  nndivlub  24897  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem5  24929  areacirclem6  24930  areacirc  24931  oriso  25214  mslb1  25607  nn0prpwlem  26238  nn0prpw  26239  seqpo  26457  incsequz2  26459  lmclim2  26474  geomcau  26475  caushft  26477  prdsbnd  26517  ismtyima  26527  heiborlem4  26538  heiborlem6  26540  heiborlem7  26541  bfplem1  26546  bfplem2  26547  rrndstprj2  26555  rrncmslem  26556  rrnequiv  26559  irrapxlem3  26909  irrapxlem4  26910  irrapxlem5  26911  irrapxlem6  26912  pellexlem3  26916  monotoddzz  27028  jm2.19  27086  rmydioph  27107  fnwe2lem2  27148  islinds  27279  lindsss  27294  hbtlem1  27327  hbtlem2  27328  hbtlem7  27329  hbtlem4  27330  hbtlem5  27332  hbtlem6  27333  dgrsub2  27339  symggen  27411  fiuneneq  27513  evth2f  27686  evthf  27698  cncmpmax  27703  rfcnpre4  27705  fmul01  27710  climinf  27732  climsuse  27734  stoweidlem7  27756  stoweidlem9  27758  stoweidlem15  27764  stoweidlem16  27765  stoweidlem18  27767  stoweidlem21  27770  stoweidlem26  27775  stoweidlem31  27780  stoweidlem34  27783  stoweidlem36  27785  stoweidlem37  27786  stoweidlem41  27790  stoweidlem44  27793  stoweidlem45  27794  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem55  27804  stoweidlem59  27808  stoweidlem60  27809  uslgra1  28118  oposlem  29373  opltcon2b  29396  pats  29475  ishlat1  29542  cvrexch  29609  atle  29625  athgt  29645  1cvrco  29661  3atlem5  29676  4atlem3  29785  dalawlem15  30074  lhprelat3N  30229  lautle  30273  lautcvr  30281  ltrnatb  30326  ltrneq2  30337  cdlemefr32sn2aw  30593  cdlemefs32sn1aw  30603  cdleme32fvaw  30628  cdleme35sn3a  30648  cdleme46frvlpq  30693  cdleme48gfv  30726  trlord  30758  cdlemg1fvawlemN  30762  cdlemg7fvbwN  30796  cdlemg31d  30889  istendo  30949  dva1dim  31174  dvhb1dimN  31175  diafval  31221  diaelval  31223  cdlemm10N  31308  dihopelvalcpre  31438  dihmeetcN  31492  dihmeetlem6  31499  dihjatc1  31501
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator