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

Theorem breq1d 4214
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 4207 . 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 1652   class class class wbr 4204
This theorem is referenced by:  eqbrtrd  4224  syl6eqbr  4241  sbcbr2g  4256  pofun  4511  dffv2  5788  fmptco  5893  isorel  6038  soisores  6039  soisoi  6040  isocnv  6042  isotr  6048  f1owe  6065  f1oweALT  6066  weniso  6067  caovordig  6244  caovordg  6246  caovord  6250  frxp  6448  xporderlem  6449  fnwelem  6453  reldmtpos  6479  brtpos  6480  tpostpos  6491  tposoprab  6507  th3qlem2  7003  ensn1g  7164  fndmeng  7175  xpsneng  7185  xpcomco  7190  pwdom  7251  ordtypelem6  7484  ordtypelem7  7485  wdompwdom  7538  infdiffi  7604  r1sdom  7692  pm54.43  7879  prdom2  7882  indcardi  7914  alephordi  7947  cdalepw  8068  fin23lem26  8197  fin23lem23  8198  fin23lem22  8199  fin23lem27  8200  uniimadomf  8412  alephval2  8439  inar1  8642  nqereu  8798  ltrnq  8848  prlem934  8902  prlem936  8916  ltasr  8967  addgt0sr  8971  axpre-ltadd  9034  axpre-sup  9036  ltsubadd  9490  lesubadd  9492  ltaddsub2  9495  leaddsub2  9497  ltaddpos  9510  lesub2  9515  ltnegcon2  9522  lenegcon2  9525  addge01  9530  subge0  9533  suble0  9534  lesub0  9536  ltordlem  9544  mulgt1  9861  ltmulgt11  9862  gt0div  9868  ge0div  9869  ltmuldiv  9872  ltmuldiv2  9873  lemuldiv2  9882  ltrec  9883  lerec2  9890  ltdiv23  9893  lediv23  9894  addltmul  10195  avglt1  10197  avgle1  10199  avgle  10201  zlem1lt  10319  rpnnen1lem5  10596  reexALT  10598  xrmin2  10758  xltnegi  10794  xmulval  10803  xlesubadd  10834  xmullem2  10836  uzenom  11296  seqf1olem1  11354  leexp2r  11429  sqlecan  11479  expmulnbnd  11503  hashbnd  11616  hashle00  11661  hashgt12el2  11675  hashf1  11698  seqcoll  11704  shftfval  11877  shftfib  11879  shftfn  11880  2shfti  11887  shftidt2  11888  sqrlem1  12040  sqrlem2  12041  sqrlem6  12045  sqrlem7  12046  absdiflt  12113  absdifle  12114  lenegsq  12116  cau3lem  12150  limsupgle  12263  limsupgre  12267  clim  12280  rlim  12281  rlim2  12282  clim2  12290  clim0  12292  clim0c  12293  rlim0  12294  rlim0lt  12295  climi0  12298  ello1  12301  ello1mpt  12307  elo1  12312  lo1o1  12318  rlimclim1  12331  rlimclim  12332  climrlim2  12333  rlimuni  12336  climuni  12338  lo1res  12345  rlimresb  12351  rlimeq  12355  2clim  12358  climshftlem  12360  climshft  12362  climabs0  12371  o1co  12372  rlimcn1  12374  rlimcn2  12376  climcn1  12377  climcn2  12378  addcn2  12379  subcn2  12380  mulcn2  12381  o1of2  12398  o1rlimmul  12404  rlimdiv  12431  rlimno1  12439  isershft  12449  isercoll  12453  climsup  12455  climcau  12456  caucvgrlem  12458  caucvgrlem2  12460  caurcvg2  12463  caucvg  12464  caucvgb  12465  serf0  12466  iseraltlem2  12468  iseralt  12470  sumeq1f  12474  sumeq2w  12478  sumeq2ii  12479  cbvsum  12481  sumrb  12499  summolem2  12502  summo  12503  zsum  12504  o1fsum  12584  cvgcmp  12587  cvgcmpce  12589  isumshft  12611  climcndslem1  12621  geolim  12639  geolim2  12640  geoisum1c  12649  mertenslem1  12653  mertenslem2  12654  mertens  12655  sin01bnd  12778  cos01bnd  12779  rpnnen  12818  ruclem9  12829  ruclem12  12832  sadcaddlem  12961  gcddvds  13007  dvdssq  13052  isprm  13073  isprm2lem  13078  isprm6  13101  isprm5  13104  odzdvds  13173  pclem  13204  pcprecl  13205  pcprendvds  13206  pcpremul  13209  pcval  13210  pceulem  13211  pczndvds  13230  pcelnn  13235  pc2dvds  13244  pcadd  13250  pcadd2  13251  pcmpt  13253  prmpwdvds  13264  prmreclem1  13276  prmreclem5  13280  prmreclem6  13281  4sqlem17  13321  vdwlem10  13350  ramval  13368  0ram  13380  ram0  13382  ramz2  13384  ramub1lem2  13387  imasaddfnlem  13745  imasvscafn  13754  imasleval  13758  mreexexlemd  13861  oddvdsnn0  15174  oddvds  15177  odf1  15190  odf1o1  15198  odf1o2  15199  gexdvds  15210  sylow1lem3  15226  efginvrel2  15351  efgsfo  15363  efgredlemd  15368  efgredlem  15371  efgred  15372  gexexlem  15459  torsubg  15461  oddvdssubg  15462  lt6abl  15496  ablfacrplem  15615  ablfacrp  15616  ablfaclem3  15637  abvfval  15898  abvpropd  15922  znf1o  16824  znidomb  16834  cygznlem1  16839  cctop  17062  ordthmeolem  17825  csdfil  17918  ufilen  17954  ptcmplem2  18076  ptcmplem3  18077  cnextfvval  18088  prdsxmetlem  18390  blfvalps  18405  elblps  18409  elbl  18410  elbl3ps  18413  elbl3  18414  blres  18453  imasf1obl  18510  blcld  18527  comet  18535  stdbdmetval  18536  stdbdbl  18539  metcnp2  18564  txmetcnp  18569  dscopn  18613  ngptgp  18669  nlmvscn  18715  nrginvrcn  18719  nmoval  18741  nghmcn  18771  cnbl0  18800  cnblcld  18801  bl2ioo  18815  recld2  18837  icccmplem2  18846  addcnlem  18886  divcn  18890  elcncf  18911  elcncf2  18912  cncfi  18916  rescncf  18919  mulc1cncf  18927  cncfco  18929  cncfmet  18930  cnheiborlem  18971  cnheibor  18972  cnllycmp  18973  evth  18976  htpycc  18997  phtpycc  19008  pcohtpylem  19036  pcoass  19041  pcorevlem  19043  nmoleub2lem2  19116  nmoleub3  19119  nmhmcn  19120  ipcau2  19183  ipcn  19192  lmmbr2  19204  lmmcvg  19206  lmmbrf  19207  fmcfil  19217  iscau2  19222  iscau4  19224  iscauf  19225  caucfil  19228  iscmet3lem3  19235  iscmet3lem1  19236  iscmet3lem2  19237  cfilresi  19240  cfilres  19241  caussi  19242  causs  19243  lmle  19246  lmclim  19247  bcthlem1  19269  bcthlem4  19272  bcth  19274  minveclem3b  19321  minveclem3  19322  minveclem4  19325  minveclem5  19326  minveclem7  19328  pmltpclem1  19337  pmltpc  19339  ivthlem1  19340  ivthlem2  19341  ivthlem3  19342  ivth  19343  cniccbdd  19350  ovolunlem1  19385  ovoliunlem1  19390  ovoliunlem2  19391  ovoliunlem3  19392  ovolshftlem1  19397  ovolscalem1  19401  ovolicc1  19404  ovolicc2lem3  19407  ovolicc2lem4  19408  ovolicc2lem5  19409  ioombl1lem4  19447  ioombl1  19448  uniioombllem6  19472  volsup2  19489  volcn  19490  mbfmulc2lem  19531  mbfsup  19548  mbflimsup  19550  itg1climres  19598  mbfi1fseqlem6  19604  mbfi1fseq  19605  mbfi1flimlem  19606  itg2leub  19618  itg2seq  19626  itg2mulclem  19630  itg2monolem1  19634  itg2mono  19637  itg2i1fseq  19639  itg2addlem  19642  itg2gt0  19644  itg2cnlem1  19645  itg2cnlem2  19646  itg2cn  19647  bddmulibl  19722  itgcn  19726  ellimc3  19758  dveflem  19855  dvferm1lem  19860  dvferm2lem  19862  rolle  19866  dvlip  19869  dvlipcn  19870  dvlip2  19871  c1liplem1  19872  c1lip3  19875  dvge0  19882  dvivthlem1  19884  lhop1lem  19889  lhop1  19890  dvcvx  19896  dvfsumabs  19899  dvfsumlem2  19903  dvfsumrlim  19907  ftc1a  19913  ftc1lem4  19915  ftc1lem6  19917  itgsubstlem  19924  mdegleb  19979  mdegmullem  19993  deg1lt0  20006  ply1divmo  20050  ply1divex  20051  ply1divalg2  20053  q1peqb  20069  fta1g  20082  dgrub  20145  coe1termlem  20168  dgrcolem2  20184  dgrco  20185  quotval  20201  plydivlem3  20204  plydivlem4  20205  plydivex  20206  plydivalg  20208  quotlem  20209  plyrem  20214  fta1  20217  aannenlem1  20237  aannenlem2  20238  aalioulem3  20243  aalioulem4  20244  aalioulem5  20245  aalioulem6  20246  aaliou  20247  aaliou2  20249  aaliou2b  20250  ulmval  20288  ulm2  20293  ulmclm  20295  ulmshftlem  20297  ulmcaulem  20302  ulmcau  20303  ulmss  20305  ulmcn  20307  ulmdvlem1  20308  ulmdvlem3  20310  mtestbdd  20313  iblulm  20315  itgulm  20316  radcnvlem1  20321  pserulm  20330  abelthlem2  20340  abelthlem5  20343  abelthlem7  20346  abelthlem8  20347  abelthlem9  20348  abelth  20349  pilem3  20361  sincosq2sgn  20399  sincosq3sgn  20400  sincosq4sgn  20401  logltb  20486  logcnlem5  20529  cxpcn3lem  20623  cxpcn3  20624  cxpaddle  20628  logreclem  20652  rlimcnp  20796  rlimcnp2  20797  xrlimcnp  20799  rlimcxp  20804  cxploglim  20808  jensen  20819  emcllem6  20831  emcllem7  20832  ftalem2  20848  ftalem3  20849  ftalem5  20851  sqfpc  20912  mumullem2  20955  sqff1o  20957  chtublem  20987  chtub  20988  fsumvma2  20990  chpchtsum  20995  logexprlim  21001  bposlem6  21065  lgslem2  21073  lgslem3  21074  lgsval  21076  lgsfcl2  21078  lgsfle1  21081  lgsle1  21087  lgsdirprm  21105  chtppilimlem2  21160  chtppilim  21161  dchrisumlema  21174  dchrisumlem1  21175  dchrisumlem2  21176  dchrisumlem3  21177  dchrisum  21178  dchrmusumlema  21179  dchrvmasumlem2  21184  dchrisum0flblem1  21194  dchrisum0lema  21200  2vmadivsumlem  21226  chpdifbndlem1  21239  selberg3lem1  21243  selberg4lem1  21246  pntrsumbnd  21252  pntrsumbnd2  21253  selbergsb  21261  pntrlog2bndlem3  21265  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntpbnd1  21272  pntpbnd2  21273  pntibndlem2  21277  pntibndlem3  21278  pntibnd  21279  pntlemn  21286  pntlemj  21289  pntlemi  21290  pntlemo  21293  pntlem3  21295  pntlemp  21296  pntleml  21297  pnt3  21298  padicabv  21316  ostth2lem2  21320  ostth3  21324  ostth  21325  umgrale  21348  umgrafi  21349  umgra1  21353  uslgra1  21384  1pthoncl  21584  2pthoncl  21595  umgrabi  21697  isnvlem  22081  nvelbl  22177  nvelbl2  22178  nmoofval  22255  nmosetn0  22258  nmoolb  22264  nmoubi  22265  nmounbseqi  22270  nmounbseqiOLD  22271  nmobndseqi  22272  nmobndseqiOLD  22273  bloval  22274  isblo  22275  nmoo0  22284  nmlno0lem  22286  blocnilem  22297  siilem2  22345  ubthlem1  22364  ubthlem2  22365  ubthlem3  22366  ubth  22367  minvecolem3  22370  minvecolem4  22374  minvecolem5  22375  minvecolem7  22377  htthlem  22412  htth  22413  h2hcau  22474  h2hlm  22475  normlem7tALT  22613  norm3lemt  22646  hcau  22678  hlimi  22682  hlim2  22686  cmcm3  23109  pjnorm  23218  pjnel  23220  elcnop  23352  elbdop  23355  nmopsetn0  23360  nmfnsetn0  23373  elcnfn  23377  hhcno  23399  hhcnf  23400  nmoplb  23402  nmopub  23403  cnopc  23408  nmfnlb  23419  nmfnleub  23420  cnfnc  23425  idcnop  23476  nmop0  23481  nmfn0  23482  nmlnop0iALT  23490  nmcexi  23521  nmcopexi  23522  lnconi  23528  lnopcon  23530  nmcfnexi  23546  lnfncon  23551  branmfn  23600  leop3  23620  opsqrlem6  23640  cvmd  23831  cvdmd  23832  cvexch  23869  cdj3i  23936  fmptcof2  24068  xraddge02  24115  xdivpnfrp  24171  isofld  24227  ofldadd  24230  ofldmul  24231  sqsscirc2  24299  cnre2csqlem  24300  xrge0iifiso  24313  lmdvg  24330  qqhcn  24367  qqhucn  24368  brfae  24591  dya2ub  24612  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemimin  24755  ballotlemic  24756  ballotlemsv  24759  ballotlemfrcn0  24779  ballotlemrc  24780  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamgulmlem5  24809  lgamgulmlem6  24810  lgambdd  24813  lgamucov  24814  lgamcvglem  24816  erdszelem8  24876  kur14  24894  snmlval  25010  snmlflim  25011  sinccvg  25102  abs2sqle  25112  abs2sqlt  25113  ntrivcvg  25217  ntrivcvgn0  25218  ntrivcvgmullem  25221  prodeq1f  25226  prodeq2w  25230  prodeq2ii  25231  prodrblem2  25249  prodmolem2  25253  prodmo  25254  zprod  25255  fprodntriv  25260  faclim2  25359  poseq  25520  soseq  25521  sltval  25594  brimg  25774  brbtwn2  25836  colinearalg  25841  axcontlem10  25904  cgrtriv  25928  cgrdegen  25930  brofs  25931  cgrextend  25934  segconeu  25937  fvtransport  25958  transportprops  25960  brifs  25969  ifscgr  25970  brcgr3  25972  cgrxfr  25981  brfs  26005  btwnconn1lem7  26019  btwnconn1lem11  26023  btwnconn1lem12  26024  btwnconn1lem14  26026  brsegle  26034  segleantisym  26041  outsideofeu  26057  nndivlub  26200  itg2addnclem  26246  itg2addnclem3  26248  itg2addnc  26249  itg2gt0cn  26250  bddiblnc  26265  ftc1cnnclem  26268  ftc1cnnc  26269  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anc  26278  areacirclem2  26282  areacirclem3  26283  areacirclem4  26284  areacirclem5  26286  areacirclem6  26287  areacirc  26288  nn0prpwlem  26316  nn0prpw  26317  seqpo  26442  incsequz2  26444  lmclim2  26455  geomcau  26456  caushft  26458  prdsbnd  26493  ismtyima  26503  heiborlem4  26514  heiborlem6  26516  heiborlem7  26517  bfplem1  26522  bfplem2  26523  rrndstprj2  26531  rrncmslem  26532  rrnequiv  26535  irrapxlem3  26878  irrapxlem4  26879  irrapxlem5  26880  irrapxlem6  26881  pellexlem3  26885  monotoddzz  26997  jm2.19  27055  rmydioph  27076  fnwe2lem2  27117  islinds  27247  lindsss  27262  hbtlem1  27295  hbtlem2  27296  hbtlem7  27297  hbtlem4  27298  hbtlem5  27300  hbtlem6  27301  dgrsub2  27307  symggen  27379  fiuneneq  27481  evth2f  27653  evthf  27665  cncmpmax  27670  rfcnpre4  27672  fmul01  27677  climinf  27699  climsuse  27701  stoweidlem7  27723  stoweidlem9  27725  stoweidlem15  27731  stoweidlem16  27732  stoweidlem18  27734  stoweidlem21  27737  stoweidlem26  27742  stoweidlem31  27747  stoweidlem34  27750  stoweidlem36  27752  stoweidlem37  27753  stoweidlem41  27757  stoweidlem44  27760  stoweidlem45  27761  stoweidlem46  27762  stoweidlem48  27764  stoweidlem51  27767  stoweidlem52  27768  stoweidlem55  27771  stoweidlem59  27775  stoweidlem60  27776  ubmelm1fzo  28110  swrdccatin2  28176  prmgt1  28189  2cshw1lem3  28216  2cshwcom  28230  cshweqdif2  28233  frgrawopreglem2  28371  oposlem  29918  opltcon2b  29941  pats  30020  ishlat1  30087  cvrexch  30154  atle  30170  athgt  30190  1cvrco  30206  3atlem5  30221  4atlem3  30330  dalawlem15  30619  lhprelat3N  30774  lautle  30818  lautcvr  30826  ltrnatb  30871  ltrneq2  30882  cdlemefr32sn2aw  31138  cdlemefs32sn1aw  31148  cdleme32fvaw  31173  cdleme35sn3a  31193  cdleme46frvlpq  31238  cdleme48gfv  31271  trlord  31303  cdlemg1fvawlemN  31307  cdlemg7fvbwN  31341  cdlemg31d  31434  istendo  31494  dva1dim  31719  dvhb1dimN  31720  diafval  31766  diaelval  31768  cdlemm10N  31853  dihopelvalcpre  31983  dihmeetcN  32037  dihmeetlem6  32044  dihjatc1  32046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator