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

Theorem breq1d 4182
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 4175 . 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 4172
This theorem is referenced by:  eqbrtrd  4192  syl6eqbr  4209  sbcbr2g  4224  pofun  4479  dffv2  5755  fmptco  5860  isorel  6005  soisores  6006  soisoi  6007  isocnv  6009  isotr  6015  f1owe  6032  f1oweALT  6033  weniso  6034  caovordig  6211  caovordg  6213  caovord  6217  frxp  6415  xporderlem  6416  fnwelem  6420  reldmtpos  6446  brtpos  6447  tpostpos  6458  tposoprab  6474  th3qlem2  6970  ensn1g  7131  fndmeng  7142  xpsneng  7152  xpcomco  7157  pwdom  7218  ordtypelem6  7448  ordtypelem7  7449  wdompwdom  7502  infdiffi  7568  r1sdom  7656  pm54.43  7843  prdom2  7846  indcardi  7878  alephordi  7911  cdalepw  8032  fin23lem26  8161  fin23lem23  8162  fin23lem22  8163  fin23lem27  8164  uniimadomf  8376  alephval2  8403  inar1  8606  nqereu  8762  ltrnq  8812  prlem934  8866  prlem936  8880  ltasr  8931  addgt0sr  8935  axpre-ltadd  8998  axpre-sup  9000  ltsubadd  9454  lesubadd  9456  ltaddsub2  9459  leaddsub2  9461  ltaddpos  9474  lesub2  9479  ltnegcon2  9486  lenegcon2  9489  addge01  9494  subge0  9497  suble0  9498  lesub0  9500  ltordlem  9508  mulgt1  9825  ltmulgt11  9826  gt0div  9832  ge0div  9833  ltmuldiv  9836  ltmuldiv2  9837  lemuldiv2  9846  ltrec  9847  lerec2  9854  ltdiv23  9857  lediv23  9858  addltmul  10159  avglt1  10161  avgle1  10163  avgle  10165  zlem1lt  10283  rpnnen1lem5  10560  reexALT  10562  xrmin2  10722  xltnegi  10758  xmulval  10767  xlesubadd  10798  xmullem2  10800  uzenom  11259  seqf1olem1  11317  leexp2r  11392  sqlecan  11442  expmulnbnd  11466  hashbnd  11579  hashle00  11624  hashgt12el2  11638  hashf1  11661  seqcoll  11667  shftfval  11840  shftfib  11842  shftfn  11843  2shfti  11850  shftidt2  11851  sqrlem1  12003  sqrlem2  12004  sqrlem6  12008  sqrlem7  12009  absdiflt  12076  absdifle  12077  lenegsq  12079  cau3lem  12113  limsupgle  12226  limsupgre  12230  clim  12243  rlim  12244  rlim2  12245  clim2  12253  clim0  12255  clim0c  12256  rlim0  12257  rlim0lt  12258  climi0  12261  ello1  12264  ello1mpt  12270  elo1  12275  lo1o1  12281  rlimclim1  12294  rlimclim  12295  climrlim2  12296  rlimuni  12299  climuni  12301  lo1res  12308  rlimresb  12314  rlimeq  12318  2clim  12321  climshftlem  12323  climshft  12325  climabs0  12334  o1co  12335  rlimcn1  12337  rlimcn2  12339  climcn1  12340  climcn2  12341  addcn2  12342  subcn2  12343  mulcn2  12344  o1of2  12361  o1rlimmul  12367  rlimdiv  12394  rlimno1  12402  isershft  12412  isercoll  12416  climsup  12418  climcau  12419  caucvgrlem  12421  caucvgrlem2  12423  caurcvg2  12426  caucvg  12427  caucvgb  12428  serf0  12429  iseraltlem2  12431  iseralt  12433  sumeq1f  12437  sumeq2w  12441  sumeq2ii  12442  cbvsum  12444  sumrb  12462  summolem2  12465  summo  12466  zsum  12467  o1fsum  12547  cvgcmp  12550  cvgcmpce  12552  isumshft  12574  climcndslem1  12584  geolim  12602  geolim2  12603  geoisum1c  12612  mertenslem1  12616  mertenslem2  12617  mertens  12618  sin01bnd  12741  cos01bnd  12742  rpnnen  12781  ruclem9  12792  ruclem12  12795  sadcaddlem  12924  gcddvds  12970  dvdssq  13015  isprm  13036  isprm2lem  13041  isprm6  13064  isprm5  13067  odzdvds  13136  pclem  13167  pcprecl  13168  pcprendvds  13169  pcpremul  13172  pcval  13173  pceulem  13174  pczndvds  13193  pcelnn  13198  pc2dvds  13207  pcadd  13213  pcadd2  13214  pcmpt  13216  prmpwdvds  13227  prmreclem1  13239  prmreclem5  13243  prmreclem6  13244  4sqlem17  13284  vdwlem10  13313  ramval  13331  0ram  13343  ram0  13345  ramz2  13347  ramub1lem2  13350  imasaddfnlem  13708  imasvscafn  13717  imasleval  13721  mreexexlemd  13824  oddvdsnn0  15137  oddvds  15140  odf1  15153  odf1o1  15161  odf1o2  15162  gexdvds  15173  sylow1lem3  15189  efginvrel2  15314  efgsfo  15326  efgredlemd  15331  efgredlem  15334  efgred  15335  gexexlem  15422  torsubg  15424  oddvdssubg  15425  lt6abl  15459  ablfacrplem  15578  ablfacrp  15579  ablfaclem3  15600  abvfval  15861  abvpropd  15885  znf1o  16787  znidomb  16797  cygznlem1  16802  cctop  17025  ordthmeolem  17786  csdfil  17879  ufilen  17915  ptcmplem2  18037  ptcmplem3  18038  cnextfvval  18049  prdsxmetlem  18351  blfvalps  18366  elblps  18370  elbl  18371  elbl3ps  18374  elbl3  18375  blres  18414  imasf1obl  18471  blcld  18488  comet  18496  stdbdmetval  18497  stdbdbl  18500  metcnp2  18525  txmetcnp  18530  dscopn  18574  ngptgp  18630  nlmvscn  18676  nrginvrcn  18680  nmoval  18702  nghmcn  18732  cnbl0  18761  cnblcld  18762  bl2ioo  18776  recld2  18798  icccmplem2  18807  addcnlem  18847  divcn  18851  elcncf  18872  elcncf2  18873  cncfi  18877  rescncf  18880  mulc1cncf  18888  cncfco  18890  cncfmet  18891  cnheiborlem  18932  cnheibor  18933  cnllycmp  18934  evth  18937  htpycc  18958  phtpycc  18969  pcohtpylem  18997  pcoass  19002  pcorevlem  19004  nmoleub2lem2  19077  nmoleub3  19080  nmhmcn  19081  ipcau2  19144  ipcn  19153  lmmbr2  19165  lmmcvg  19167  lmmbrf  19168  fmcfil  19178  iscau2  19183  iscau4  19185  iscauf  19186  caucfil  19189  iscmet3lem3  19196  iscmet3lem1  19197  iscmet3lem2  19198  cfilresi  19201  cfilres  19202  caussi  19203  causs  19204  lmle  19207  lmclim  19208  bcthlem1  19230  bcthlem4  19233  bcth  19235  minveclem3b  19282  minveclem3  19283  minveclem4  19286  minveclem5  19287  minveclem7  19289  pmltpclem1  19298  pmltpc  19300  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ivth  19304  cniccbdd  19311  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliunlem3  19353  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ioombl1lem4  19408  ioombl1  19409  uniioombllem6  19433  volsup2  19450  volcn  19451  mbfmulc2lem  19492  mbfsup  19509  mbflimsup  19511  itg1climres  19559  mbfi1fseqlem6  19565  mbfi1fseq  19566  mbfi1flimlem  19567  itg2leub  19579  itg2seq  19587  itg2mulclem  19591  itg2monolem1  19595  itg2mono  19598  itg2i1fseq  19600  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  bddmulibl  19683  itgcn  19687  ellimc3  19719  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  rolle  19827  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  c1lip3  19836  dvge0  19843  dvivthlem1  19845  lhop1lem  19850  lhop1  19851  dvcvx  19857  dvfsumabs  19860  dvfsumlem2  19864  dvfsumrlim  19868  ftc1a  19874  ftc1lem4  19876  ftc1lem6  19878  itgsubstlem  19885  mdegleb  19940  mdegmullem  19954  deg1lt0  19967  ply1divmo  20011  ply1divex  20012  ply1divalg2  20014  q1peqb  20030  fta1g  20043  dgrub  20106  coe1termlem  20129  dgrcolem2  20145  dgrco  20146  quotval  20162  plydivlem3  20165  plydivlem4  20166  plydivex  20167  plydivalg  20169  quotlem  20170  plyrem  20175  fta1  20178  aannenlem1  20198  aannenlem2  20199  aalioulem3  20204  aalioulem4  20205  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou2  20210  aaliou2b  20211  ulmval  20249  ulm2  20254  ulmclm  20256  ulmshftlem  20258  ulmcaulem  20263  ulmcau  20264  ulmss  20266  ulmcn  20268  ulmdvlem1  20269  ulmdvlem3  20271  mtestbdd  20274  iblulm  20276  itgulm  20277  radcnvlem1  20282  pserulm  20291  abelthlem2  20301  abelthlem5  20304  abelthlem7  20307  abelthlem8  20308  abelthlem9  20309  abelth  20310  pilem3  20322  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  logltb  20447  logcnlem5  20490  cxpcn3lem  20584  cxpcn3  20585  cxpaddle  20589  logreclem  20613  rlimcnp  20757  rlimcnp2  20758  xrlimcnp  20760  rlimcxp  20765  cxploglim  20769  jensen  20780  emcllem6  20792  emcllem7  20793  ftalem2  20809  ftalem3  20810  ftalem5  20812  sqfpc  20873  mumullem2  20916  sqff1o  20918  chtublem  20948  chtub  20949  fsumvma2  20951  chpchtsum  20956  logexprlim  20962  bposlem6  21026  lgslem2  21034  lgslem3  21035  lgsval  21037  lgsfcl2  21039  lgsfle1  21042  lgsle1  21048  lgsdirprm  21066  chtppilimlem2  21121  chtppilim  21122  dchrisumlema  21135  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrisum  21139  dchrmusumlema  21140  dchrvmasumlem2  21145  dchrisum0flblem1  21155  dchrisum0lema  21161  2vmadivsumlem  21187  chpdifbndlem1  21200  selberg3lem1  21204  selberg4lem1  21207  pntrsumbnd  21213  pntrsumbnd2  21214  selbergsb  21222  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemn  21247  pntlemj  21250  pntlemi  21251  pntlemo  21254  pntlem3  21256  pntlemp  21257  pntleml  21258  pnt3  21259  padicabv  21277  ostth2lem2  21281  ostth3  21285  ostth  21286  umgrale  21309  umgrafi  21310  umgra1  21314  uslgra1  21345  1pthoncl  21545  2pthoncl  21556  umgrabi  21658  isnvlem  22042  nvelbl  22138  nvelbl2  22139  nmoofval  22216  nmosetn0  22219  nmoolb  22225  nmoubi  22226  nmounbseqi  22231  nmounbseqiOLD  22232  nmobndseqi  22233  nmobndseqiOLD  22234  bloval  22235  isblo  22236  nmoo0  22245  nmlno0lem  22247  blocnilem  22258  siilem2  22306  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  ubth  22328  minvecolem3  22331  minvecolem4  22335  minvecolem5  22336  minvecolem7  22338  htthlem  22373  htth  22374  h2hcau  22435  h2hlm  22436  normlem7tALT  22574  norm3lemt  22607  hcau  22639  hlimi  22643  hlim2  22647  cmcm3  23070  pjnorm  23179  pjnel  23181  elcnop  23313  elbdop  23316  nmopsetn0  23321  nmfnsetn0  23334  elcnfn  23338  hhcno  23360  hhcnf  23361  nmoplb  23363  nmopub  23364  cnopc  23369  nmfnlb  23380  nmfnleub  23381  cnfnc  23386  idcnop  23437  nmop0  23442  nmfn0  23443  nmlnop0iALT  23451  nmcexi  23482  nmcopexi  23483  lnconi  23489  lnopcon  23491  nmcfnexi  23507  lnfncon  23512  branmfn  23561  leop3  23581  opsqrlem6  23601  cvmd  23792  cvdmd  23793  cvexch  23830  cdj3i  23897  fmptcof2  24029  xraddge02  24076  xdivpnfrp  24132  isofld  24188  ofldadd  24191  ofldmul  24192  sqsscirc2  24260  cnre2csqlem  24261  xrge0iifiso  24274  lmdvg  24291  qqhcn  24328  qqhucn  24329  brfae  24552  dya2ub  24573  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemimin  24716  ballotlemic  24717  ballotlemsv  24720  ballotlemfrcn0  24740  ballotlemrc  24741  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgamgulmlem6  24771  lgambdd  24774  lgamucov  24775  lgamcvglem  24777  erdszelem8  24837  kur14  24855  snmlval  24971  snmlflim  24972  sinccvg  25063  abs2sqle  25073  abs2sqlt  25074  ntrivcvg  25178  ntrivcvgn0  25179  ntrivcvgmullem  25182  prodeq1f  25187  prodeq2w  25191  prodeq2ii  25192  prodrblem2  25210  prodmolem2  25214  prodmo  25215  zprod  25216  fprodntriv  25221  faclim2  25315  poseq  25467  soseq  25468  sltval  25515  brimg  25690  brbtwn2  25748  colinearalg  25753  axcontlem10  25816  cgrtriv  25840  cgrdegen  25842  brofs  25843  cgrextend  25846  segconeu  25849  fvtransport  25870  transportprops  25872  brifs  25881  ifscgr  25882  brcgr3  25884  cgrxfr  25893  brfs  25917  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn1lem14  25938  brsegle  25946  segleantisym  25953  outsideofeu  25969  nndivlub  26112  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  bddiblnc  26174  ftc1cnnclem  26177  ftc1cnnc  26178  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  areacirclem5  26185  areacirclem6  26186  areacirc  26187  nn0prpwlem  26215  nn0prpw  26216  seqpo  26341  incsequz2  26343  lmclim2  26354  geomcau  26355  caushft  26357  prdsbnd  26392  ismtyima  26402  heiborlem4  26413  heiborlem6  26415  heiborlem7  26416  bfplem1  26421  bfplem2  26422  rrndstprj2  26430  rrncmslem  26431  rrnequiv  26434  irrapxlem3  26777  irrapxlem4  26778  irrapxlem5  26779  irrapxlem6  26780  pellexlem3  26784  monotoddzz  26896  jm2.19  26954  rmydioph  26975  fnwe2lem2  27016  islinds  27147  lindsss  27162  hbtlem1  27195  hbtlem2  27196  hbtlem7  27197  hbtlem4  27198  hbtlem5  27200  hbtlem6  27201  dgrsub2  27207  symggen  27279  fiuneneq  27381  evth2f  27553  evthf  27565  cncmpmax  27570  rfcnpre4  27572  fmul01  27577  climinf  27599  climsuse  27601  stoweidlem7  27623  stoweidlem9  27625  stoweidlem15  27631  stoweidlem16  27632  stoweidlem18  27634  stoweidlem21  27637  stoweidlem26  27642  stoweidlem31  27647  stoweidlem34  27650  stoweidlem36  27652  stoweidlem37  27653  stoweidlem41  27657  stoweidlem44  27660  stoweidlem45  27661  stoweidlem46  27662  stoweidlem48  27664  stoweidlem51  27667  stoweidlem52  27668  stoweidlem55  27671  stoweidlem59  27675  stoweidlem60  27676  ubmelm1fzo  27987  swrdccat3b  28031  frgrawopreglem2  28148  oposlem  29666  opltcon2b  29689  pats  29768  ishlat1  29835  cvrexch  29902  atle  29918  athgt  29938  1cvrco  29954  3atlem5  29969  4atlem3  30078  dalawlem15  30367  lhprelat3N  30522  lautle  30566  lautcvr  30574  ltrnatb  30619  ltrneq2  30630  cdlemefr32sn2aw  30886  cdlemefs32sn1aw  30896  cdleme32fvaw  30921  cdleme35sn3a  30941  cdleme46frvlpq  30986  cdleme48gfv  31019  trlord  31051  cdlemg1fvawlemN  31055  cdlemg7fvbwN  31089  cdlemg31d  31182  istendo  31242  dva1dim  31467  dvhb1dimN  31468  diafval  31514  diaelval  31516  cdlemm10N  31601  dihopelvalcpre  31731  dihmeetcN  31785  dihmeetlem6  31792  dihjatc1  31794
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator