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

Theorem breq1d 4035
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 4028 . 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 1625   class class class wbr 4025
This theorem is referenced by:  eqbrtrd  4045  syl6eqbr  4062  sbcbr2g  4077  pofun  4332  dffv2  5594  fmptco  5693  isorel  5825  soisores  5826  soisoi  5827  isocnv  5829  isotr  5835  f1owe  5852  f1oweALT  5853  weniso  5854  caovordig  6027  caovordg  6029  caovord  6033  frxp  6227  xporderlem  6228  fnwelem  6232  reldmtpos  6244  brtpos  6245  tpostpos  6256  tposoprab  6272  th3qlem2  6767  ensn1g  6928  fndmeng  6939  xpsneng  6949  xpcomco  6954  pwdom  7015  ordtypelem6  7240  ordtypelem7  7241  wdompwdom  7294  infdiffi  7360  r1sdom  7448  pm54.43  7635  prdom2  7638  indcardi  7670  alephordi  7703  cdalepw  7824  fin23lem26  7953  fin23lem23  7954  fin23lem22  7955  fin23lem27  7956  uniimadomf  8169  alephval2  8196  inar1  8399  nqereu  8555  ltrnq  8605  prlem934  8659  prlem936  8673  ltasr  8724  addgt0sr  8728  axpre-ltadd  8791  axpre-sup  8793  ltsubadd  9246  lesubadd  9248  ltaddsub2  9251  leaddsub2  9253  ltaddpos  9266  lesub2  9271  ltnegcon2  9278  lenegcon2  9281  addge01  9286  subge0  9289  suble0  9290  lesub0  9292  ltordlem  9300  mulgt1  9617  ltmulgt11  9618  gt0div  9624  ge0div  9625  ltmuldiv  9628  ltmuldiv2  9629  lemuldiv2  9638  ltrec  9639  lerec2  9646  ltdiv23  9649  lediv23  9650  addltmul  9949  avglt1  9951  avgle1  9953  avgle  9955  zlem1lt  10071  rpnnen1lem5  10348  reexALT  10350  xrmin2  10509  xltnegi  10545  xmulval  10554  xlesubadd  10585  xmullem2  10587  uzenom  11029  seqf1olem1  11087  leexp2r  11161  sqlecan  11211  expmulnbnd  11235  hashbnd  11345  hashf1  11397  seqcoll  11403  shftfval  11567  shftfib  11569  shftfn  11570  2shfti  11577  shftidt2  11578  sqrlem1  11730  sqrlem2  11731  sqrlem6  11735  sqrlem7  11736  absdiflt  11803  absdifle  11804  lenegsq  11806  cau3lem  11840  limsupgle  11953  limsupgre  11957  clim  11970  rlim  11971  rlim2  11972  clim2  11980  clim0  11982  clim0c  11983  rlim0  11984  rlim0lt  11985  climi0  11988  ello1  11991  ello1mpt  11997  elo1  12002  lo1o1  12008  rlimclim1  12021  rlimclim  12022  climrlim2  12023  rlimuni  12026  climuni  12028  lo1res  12035  rlimresb  12041  rlimeq  12045  2clim  12048  climshftlem  12050  climshft  12052  climabs0  12061  o1co  12062  rlimcn1  12064  rlimcn2  12066  climcn1  12067  climcn2  12068  addcn2  12069  subcn2  12070  mulcn2  12071  o1of2  12088  o1rlimmul  12094  rlimdiv  12121  rlimno1  12129  isershft  12139  isercoll  12143  climsup  12145  climcau  12146  caucvgrlem  12147  caucvgrlem2  12149  caurcvg2  12152  caucvg  12153  caucvgb  12154  serf0  12155  iseraltlem2  12157  iseralt  12159  sumeq1f  12163  sumeq2w  12167  sumeq2ii  12168  cbvsum  12170  sumrb  12188  summolem2  12191  summo  12192  zsum  12193  o1fsum  12273  cvgcmp  12276  cvgcmpce  12278  isumshft  12300  climcndslem1  12310  geolim  12328  geolim2  12329  geoisum1c  12338  mertenslem1  12342  mertenslem2  12343  mertens  12344  sin01bnd  12467  cos01bnd  12468  rpnnen  12507  ruclem9  12518  ruclem12  12521  sadcaddlem  12650  gcddvds  12696  dvdssq  12741  isprm  12762  isprm2lem  12767  isprm6  12790  isprm5  12793  odzdvds  12862  pclem  12893  pcprecl  12894  pcprendvds  12895  pcpremul  12898  pcval  12899  pceulem  12900  pczndvds  12919  pcelnn  12924  pc2dvds  12933  pcadd  12939  pcadd2  12940  pcmpt  12942  prmpwdvds  12953  prmreclem1  12965  prmreclem5  12969  prmreclem6  12970  4sqlem17  13010  vdwlem10  13039  ramval  13057  0ram  13069  ram0  13071  ramz2  13073  ramub1lem2  13076  imasaddfnlem  13432  imasvscafn  13441  imasleval  13445  mreexexlemd  13548  oddvdsnn0  14861  oddvds  14864  odf1  14877  odf1o1  14885  odf1o2  14886  gexdvds  14897  sylow1lem3  14913  efginvrel2  15038  efgsfo  15050  efgredlemd  15055  efgredlem  15058  efgred  15059  gexexlem  15146  torsubg  15148  oddvdssubg  15149  lt6abl  15183  ablfacrplem  15302  ablfacrp  15303  ablfaclem3  15324  abvfval  15585  abvpropd  15609  znf1o  16507  znidomb  16517  cygznlem1  16522  cctop  16745  ordthmeolem  17494  csdfil  17591  ufilen  17627  ptcmplem2  17749  ptcmplem3  17750  prdsxmetlem  17934  blfval  17949  elbl  17951  elbl3  17953  blres  17979  imasf1obl  18036  blcld  18053  comet  18061  stdbdmetval  18062  stdbdbl  18065  metcnp2  18090  txmetcnp  18095  dscopn  18098  ngptgp  18154  nlmvscn  18200  nrginvrcn  18204  nmoval  18226  nghmcn  18256  cnbl0  18285  cnblcld  18286  bl2ioo  18300  recld2  18322  icccmplem2  18330  addcnlem  18370  divcn  18374  elcncf  18395  elcncf2  18396  cncfi  18400  rescncf  18403  mulc1cncf  18411  cncfco  18413  cncfmet  18414  cnheiborlem  18454  cnheibor  18455  cnllycmp  18456  evth  18459  htpycc  18480  phtpycc  18491  pcohtpylem  18519  pcoass  18524  pcorevlem  18526  nmoleub2lem2  18599  nmoleub3  18602  nmhmcn  18603  ipcau2  18666  ipcn  18675  lmmbr2  18687  lmmcvg  18689  lmmbrf  18690  fmcfil  18700  iscau2  18705  iscau4  18707  iscauf  18708  caucfil  18711  iscmet3lem3  18718  iscmet3lem1  18719  iscmet3lem2  18720  cfilresi  18723  cfilres  18724  caussi  18725  causs  18726  lmle  18729  lmclim  18730  bcthlem1  18748  bcthlem4  18751  bcth  18753  minveclem3b  18794  minveclem3  18795  minveclem4  18798  minveclem5  18799  minveclem7  18801  pmltpclem1  18810  pmltpc  18812  ivthlem1  18813  ivthlem2  18814  ivthlem3  18815  ivth  18816  cniccbdd  18823  ovolunlem1  18858  ovoliunlem1  18863  ovoliunlem2  18864  ovoliunlem3  18865  ovolshftlem1  18870  ovolscalem1  18874  ovolicc1  18877  ovolicc2lem3  18880  ovolicc2lem4  18881  ovolicc2lem5  18882  ioombl1lem4  18920  ioombl1  18921  uniioombllem6  18945  volsup2  18962  volcn  18963  mbfmulc2lem  19004  mbfsup  19021  mbflimsup  19023  itg1climres  19071  mbfi1fseqlem6  19077  mbfi1fseq  19078  mbfi1flimlem  19079  itg2leub  19091  itg2seq  19099  itg2mulclem  19103  itg2monolem1  19107  itg2mono  19110  itg2i1fseq  19112  itg2addlem  19115  itg2gt0  19117  itg2cnlem1  19118  itg2cnlem2  19119  itg2cn  19120  bddmulibl  19195  itgcn  19199  ellimc3  19231  dveflem  19328  dvferm1lem  19333  dvferm2lem  19335  rolle  19339  dvlip  19342  dvlipcn  19343  dvlip2  19344  c1liplem1  19345  c1lip3  19348  dvge0  19355  dvivthlem1  19357  lhop1lem  19362  lhop1  19363  dvcvx  19369  dvfsumabs  19372  dvfsumlem2  19376  dvfsumrlim  19380  ftc1a  19386  ftc1lem4  19388  ftc1lem6  19390  itgsubstlem  19397  mdegleb  19452  mdegmullem  19466  deg1lt0  19479  ply1divmo  19523  ply1divex  19524  ply1divalg2  19526  q1peqb  19542  fta1g  19555  dgrub  19618  coe1termlem  19641  dgrcolem2  19657  dgrco  19658  quotval  19674  plydivlem3  19677  plydivlem4  19678  plydivex  19679  plydivalg  19681  quotlem  19682  plyrem  19687  fta1  19690  aannenlem1  19710  aannenlem2  19711  aalioulem3  19716  aalioulem4  19717  aalioulem5  19718  aalioulem6  19719  aaliou  19720  aaliou2  19722  aaliou2b  19723  ulmval  19761  ulm2  19766  ulmclm  19768  ulmshftlem  19770  ulmcaulem  19773  ulmcau  19774  ulmss  19776  ulmcn  19778  ulmdvlem1  19779  ulmdvlem3  19781  iblulm  19785  itgulm  19786  radcnvlem1  19791  pserulm  19800  abelthlem2  19810  abelthlem5  19813  abelthlem7  19816  abelthlem8  19817  abelthlem9  19818  abelth  19819  pilem3  19831  sincosq2sgn  19869  sincosq3sgn  19870  sincosq4sgn  19871  logltb  19955  logcnlem5  19995  cxpcn3lem  20089  cxpcn3  20090  cxpaddle  20094  logreclem  20118  rlimcnp  20262  rlimcnp2  20263  xrlimcnp  20265  rlimcxp  20270  cxploglim  20274  jensen  20285  emcllem6  20296  emcllem7  20297  ftalem2  20313  ftalem3  20314  ftalem5  20316  sqfpc  20377  mumullem2  20420  sqff1o  20422  chtublem  20452  chtub  20453  fsumvma2  20455  chpchtsum  20460  logexprlim  20466  bposlem6  20530  lgslem2  20538  lgslem3  20539  lgsval  20541  lgsfcl2  20543  lgsfle1  20546  lgsle1  20552  lgsdirprm  20570  chtppilimlem2  20625  chtppilim  20626  dchrisumlema  20639  dchrisumlem1  20640  dchrisumlem2  20641  dchrisumlem3  20642  dchrisum  20643  dchrmusumlema  20644  dchrvmasumlem2  20649  dchrisum0flblem1  20659  dchrisum0lema  20665  2vmadivsumlem  20691  chpdifbndlem1  20704  selberg3lem1  20708  selberg4lem1  20711  pntrsumbnd  20717  pntrsumbnd2  20718  selbergsb  20726  pntrlog2bndlem3  20730  pntrlog2bndlem5  20732  pntrlog2bndlem6  20734  pntpbnd1  20737  pntpbnd2  20738  pntibndlem2  20742  pntibndlem3  20743  pntibnd  20744  pntlemn  20751  pntlemj  20754  pntlemi  20755  pntlemo  20758  pntlem3  20760  pntlemp  20761  pntleml  20762  pnt3  20763  padicabv  20781  ostth2lem2  20785  ostth3  20789  ostth  20790  isnvlem  21168  nvelbl  21264  nvelbl2  21265  nmoofval  21342  nmosetn0  21345  nmoolb  21351  nmoubi  21352  nmounbseqi  21357  nmounbseqiOLD  21358  nmobndseqi  21359  nmobndseqiOLD  21360  bloval  21361  isblo  21362  nmoo0  21371  nmlno0lem  21373  blocnilem  21384  siilem2  21432  ubthlem1  21451  ubthlem2  21452  ubthlem3  21453  ubth  21454  minvecolem3  21457  minvecolem4  21461  minvecolem5  21462  minvecolem7  21464  htthlem  21499  htth  21500  h2hcau  21561  h2hlm  21562  normlem7tALT  21700  norm3lemt  21733  hcau  21765  hlimi  21769  hlim2  21773  cmcm3  22196  pjnorm  22305  pjnel  22307  elcnop  22439  elbdop  22442  nmopsetn0  22447  nmfnsetn0  22460  elcnfn  22464  hhcno  22486  hhcnf  22487  nmoplb  22489  nmopub  22490  cnopc  22495  nmfnlb  22506  nmfnleub  22507  cnfnc  22512  idcnop  22563  nmop0  22568  nmfn0  22569  nmlnop0iALT  22577  nmcexi  22608  nmcopexi  22609  lnconi  22615  lnopcon  22617  nmcfnexi  22633  lnfncon  22638  branmfn  22687  leop3  22707  opsqrlem6  22727  cvmd  22918  cvdmd  22919  cvexch  22956  cdj3i  23023  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemimin  23066  ballotlemic  23067  ballotlem1c  23068  ballotlemsv  23070  ballotlemfrcn0  23090  ballotlemrc  23091  xdivpnfrp  23119  fmptcof2  23231  xraddge02  23254  sqsscirc2  23295  cnre2csqlem  23296  xrge0iifiso  23319  lmdvg  23378  dya2ub  23577  erdszelem8  23731  kur14  23749  umgrale  23875  umgrafi  23876  umgra1  23880  umgrabi  23909  snmlval  23916  snmlflim  23917  sinccvg  24008  abs2sqle  24018  abs2sqlt  24019  poseq  24255  soseq  24256  sltval  24303  brimg  24478  brbtwn2  24535  colinearalg  24540  axcontlem10  24603  cgrtriv  24627  cgrdegen  24629  brofs  24630  cgrextend  24633  segconeu  24636  fvtransport  24657  transportprops  24659  brifs  24668  ifscgr  24669  brcgr3  24671  cgrxfr  24680  brfs  24704  btwnconn1lem7  24718  btwnconn1lem11  24722  btwnconn1lem12  24723  btwnconn1lem14  24725  brsegle  24733  segleantisym  24740  outsideofeu  24756  nndivlub  24899  itg2addnclem  24933  itg2addnc  24935  areacirclem2  24936  areacirclem3  24937  areacirclem4  24938  areacirclem5  24940  areacirclem6  24941  areacirc  24942  oriso  25225  mslb1  25618  nn0prpwlem  26249  nn0prpw  26250  seqpo  26468  incsequz2  26470  lmclim2  26485  geomcau  26486  caushft  26488  prdsbnd  26528  ismtyima  26538  heiborlem4  26549  heiborlem6  26551  heiborlem7  26552  bfplem1  26557  bfplem2  26558  rrndstprj2  26566  rrncmslem  26567  rrnequiv  26570  irrapxlem3  26920  irrapxlem4  26921  irrapxlem5  26922  irrapxlem6  26923  pellexlem3  26927  monotoddzz  27039  jm2.19  27097  rmydioph  27118  fnwe2lem2  27159  islinds  27290  lindsss  27305  hbtlem1  27338  hbtlem2  27339  hbtlem7  27340  hbtlem4  27341  hbtlem5  27343  hbtlem6  27344  dgrsub2  27350  symggen  27422  fiuneneq  27524  evth2f  27697  evthf  27709  cncmpmax  27714  rfcnpre4  27716  fmul01  27721  climinf  27743  climsuse  27745  stoweidlem7  27767  stoweidlem9  27769  stoweidlem15  27775  stoweidlem16  27776  stoweidlem18  27778  stoweidlem21  27781  stoweidlem26  27786  stoweidlem31  27791  stoweidlem34  27794  stoweidlem36  27796  stoweidlem37  27797  stoweidlem41  27801  stoweidlem44  27804  stoweidlem45  27805  stoweidlem46  27806  stoweidlem48  27808  stoweidlem51  27811  stoweidlem52  27812  stoweidlem55  27815  stoweidlem59  27819  stoweidlem60  27820  uslgra1  28129  oposlem  29446  opltcon2b  29469  pats  29548  ishlat1  29615  cvrexch  29682  atle  29698  athgt  29718  1cvrco  29734  3atlem5  29749  4atlem3  29858  dalawlem15  30147  lhprelat3N  30302  lautle  30346  lautcvr  30354  ltrnatb  30399  ltrneq2  30410  cdlemefr32sn2aw  30666  cdlemefs32sn1aw  30676  cdleme32fvaw  30701  cdleme35sn3a  30721  cdleme46frvlpq  30766  cdleme48gfv  30799  trlord  30831  cdlemg1fvawlemN  30835  cdlemg7fvbwN  30869  cdlemg31d  30962  istendo  31022  dva1dim  31247  dvhb1dimN  31248  diafval  31294  diaelval  31296  cdlemm10N  31381  dihopelvalcpre  31511  dihmeetcN  31565  dihmeetlem6  31572  dihjatc1  31574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026
  Copyright terms: Public domain W3C validator