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

Theorem breq1d 4049
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 4042 . 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 1632   class class class wbr 4039
This theorem is referenced by:  eqbrtrd  4059  syl6eqbr  4076  sbcbr2g  4091  pofun  4346  dffv2  5608  fmptco  5707  isorel  5839  soisores  5840  soisoi  5841  isocnv  5843  isotr  5849  f1owe  5866  f1oweALT  5867  weniso  5868  caovordig  6041  caovordg  6043  caovord  6047  frxp  6241  xporderlem  6242  fnwelem  6246  reldmtpos  6258  brtpos  6259  tpostpos  6270  tposoprab  6286  th3qlem2  6781  ensn1g  6942  fndmeng  6953  xpsneng  6963  xpcomco  6968  pwdom  7029  ordtypelem6  7254  ordtypelem7  7255  wdompwdom  7308  infdiffi  7374  r1sdom  7462  pm54.43  7649  prdom2  7652  indcardi  7684  alephordi  7717  cdalepw  7838  fin23lem26  7967  fin23lem23  7968  fin23lem22  7969  fin23lem27  7970  uniimadomf  8183  alephval2  8210  inar1  8413  nqereu  8569  ltrnq  8619  prlem934  8673  prlem936  8687  ltasr  8738  addgt0sr  8742  axpre-ltadd  8805  axpre-sup  8807  ltsubadd  9260  lesubadd  9262  ltaddsub2  9265  leaddsub2  9267  ltaddpos  9280  lesub2  9285  ltnegcon2  9292  lenegcon2  9295  addge01  9300  subge0  9303  suble0  9304  lesub0  9306  ltordlem  9314  mulgt1  9631  ltmulgt11  9632  gt0div  9638  ge0div  9639  ltmuldiv  9642  ltmuldiv2  9643  lemuldiv2  9652  ltrec  9653  lerec2  9660  ltdiv23  9663  lediv23  9664  addltmul  9963  avglt1  9965  avgle1  9967  avgle  9969  zlem1lt  10085  rpnnen1lem5  10362  reexALT  10364  xrmin2  10523  xltnegi  10559  xmulval  10568  xlesubadd  10599  xmullem2  10601  uzenom  11043  seqf1olem1  11101  leexp2r  11175  sqlecan  11225  expmulnbnd  11249  hashbnd  11359  hashf1  11411  seqcoll  11417  shftfval  11581  shftfib  11583  shftfn  11584  2shfti  11591  shftidt2  11592  sqrlem1  11744  sqrlem2  11745  sqrlem6  11749  sqrlem7  11750  absdiflt  11817  absdifle  11818  lenegsq  11820  cau3lem  11854  limsupgle  11967  limsupgre  11971  clim  11984  rlim  11985  rlim2  11986  clim2  11994  clim0  11996  clim0c  11997  rlim0  11998  rlim0lt  11999  climi0  12002  ello1  12005  ello1mpt  12011  elo1  12016  lo1o1  12022  rlimclim1  12035  rlimclim  12036  climrlim2  12037  rlimuni  12040  climuni  12042  lo1res  12049  rlimresb  12055  rlimeq  12059  2clim  12062  climshftlem  12064  climshft  12066  climabs0  12075  o1co  12076  rlimcn1  12078  rlimcn2  12080  climcn1  12081  climcn2  12082  addcn2  12083  subcn2  12084  mulcn2  12085  o1of2  12102  o1rlimmul  12108  rlimdiv  12135  rlimno1  12143  isershft  12153  isercoll  12157  climsup  12159  climcau  12160  caucvgrlem  12161  caucvgrlem2  12163  caurcvg2  12166  caucvg  12167  caucvgb  12168  serf0  12169  iseraltlem2  12171  iseralt  12173  sumeq1f  12177  sumeq2w  12181  sumeq2ii  12182  cbvsum  12184  sumrb  12202  summolem2  12205  summo  12206  zsum  12207  o1fsum  12287  cvgcmp  12290  cvgcmpce  12292  isumshft  12314  climcndslem1  12324  geolim  12342  geolim2  12343  geoisum1c  12352  mertenslem1  12356  mertenslem2  12357  mertens  12358  sin01bnd  12481  cos01bnd  12482  rpnnen  12521  ruclem9  12532  ruclem12  12535  sadcaddlem  12664  gcddvds  12710  dvdssq  12755  isprm  12776  isprm2lem  12781  isprm6  12804  isprm5  12807  odzdvds  12876  pclem  12907  pcprecl  12908  pcprendvds  12909  pcpremul  12912  pcval  12913  pceulem  12914  pczndvds  12933  pcelnn  12938  pc2dvds  12947  pcadd  12953  pcadd2  12954  pcmpt  12956  prmpwdvds  12967  prmreclem1  12979  prmreclem5  12983  prmreclem6  12984  4sqlem17  13024  vdwlem10  13053  ramval  13071  0ram  13083  ram0  13085  ramz2  13087  ramub1lem2  13090  imasaddfnlem  13446  imasvscafn  13455  imasleval  13459  mreexexlemd  13562  oddvdsnn0  14875  oddvds  14878  odf1  14891  odf1o1  14899  odf1o2  14900  gexdvds  14911  sylow1lem3  14927  efginvrel2  15052  efgsfo  15064  efgredlemd  15069  efgredlem  15072  efgred  15073  gexexlem  15160  torsubg  15162  oddvdssubg  15163  lt6abl  15197  ablfacrplem  15316  ablfacrp  15317  ablfaclem3  15338  abvfval  15599  abvpropd  15623  znf1o  16521  znidomb  16531  cygznlem1  16536  cctop  16759  ordthmeolem  17508  csdfil  17605  ufilen  17641  ptcmplem2  17763  ptcmplem3  17764  prdsxmetlem  17948  blfval  17963  elbl  17965  elbl3  17967  blres  17993  imasf1obl  18050  blcld  18067  comet  18075  stdbdmetval  18076  stdbdbl  18079  metcnp2  18104  txmetcnp  18109  dscopn  18112  ngptgp  18168  nlmvscn  18214  nrginvrcn  18218  nmoval  18240  nghmcn  18270  cnbl0  18299  cnblcld  18300  bl2ioo  18314  recld2  18336  icccmplem2  18344  addcnlem  18384  divcn  18388  elcncf  18409  elcncf2  18410  cncfi  18414  rescncf  18417  mulc1cncf  18425  cncfco  18427  cncfmet  18428  cnheiborlem  18468  cnheibor  18469  cnllycmp  18470  evth  18473  htpycc  18494  phtpycc  18505  pcohtpylem  18533  pcoass  18538  pcorevlem  18540  nmoleub2lem2  18613  nmoleub3  18616  nmhmcn  18617  ipcau2  18680  ipcn  18689  lmmbr2  18701  lmmcvg  18703  lmmbrf  18704  fmcfil  18714  iscau2  18719  iscau4  18721  iscauf  18722  caucfil  18725  iscmet3lem3  18732  iscmet3lem1  18733  iscmet3lem2  18734  cfilresi  18737  cfilres  18738  caussi  18739  causs  18740  lmle  18743  lmclim  18744  bcthlem1  18762  bcthlem4  18765  bcth  18767  minveclem3b  18808  minveclem3  18809  minveclem4  18812  minveclem5  18813  minveclem7  18815  pmltpclem1  18824  pmltpc  18826  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  ivth  18830  cniccbdd  18837  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovoliunlem3  18879  ovolshftlem1  18884  ovolscalem1  18888  ovolicc1  18891  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  ioombl1lem4  18934  ioombl1  18935  uniioombllem6  18959  volsup2  18976  volcn  18977  mbfmulc2lem  19018  mbfsup  19035  mbflimsup  19037  itg1climres  19085  mbfi1fseqlem6  19091  mbfi1fseq  19092  mbfi1flimlem  19093  itg2leub  19105  itg2seq  19113  itg2mulclem  19117  itg2monolem1  19121  itg2mono  19124  itg2i1fseq  19126  itg2addlem  19129  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  bddmulibl  19209  itgcn  19213  ellimc3  19245  dveflem  19342  dvferm1lem  19347  dvferm2lem  19349  rolle  19353  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  c1lip3  19362  dvge0  19369  dvivthlem1  19371  lhop1lem  19376  lhop1  19377  dvcvx  19383  dvfsumabs  19386  dvfsumlem2  19390  dvfsumrlim  19394  ftc1a  19400  ftc1lem4  19402  ftc1lem6  19404  itgsubstlem  19411  mdegleb  19466  mdegmullem  19480  deg1lt0  19493  ply1divmo  19537  ply1divex  19538  ply1divalg2  19540  q1peqb  19556  fta1g  19569  dgrub  19632  coe1termlem  19655  dgrcolem2  19671  dgrco  19672  quotval  19688  plydivlem3  19691  plydivlem4  19692  plydivex  19693  plydivalg  19695  quotlem  19696  plyrem  19701  fta1  19704  aannenlem1  19724  aannenlem2  19725  aalioulem3  19730  aalioulem4  19731  aalioulem5  19732  aalioulem6  19733  aaliou  19734  aaliou2  19736  aaliou2b  19737  ulmval  19775  ulm2  19780  ulmclm  19782  ulmshftlem  19784  ulmcaulem  19787  ulmcau  19788  ulmss  19790  ulmcn  19792  ulmdvlem1  19793  ulmdvlem3  19795  iblulm  19799  itgulm  19800  radcnvlem1  19805  pserulm  19814  abelthlem2  19824  abelthlem5  19827  abelthlem7  19830  abelthlem8  19831  abelthlem9  19832  abelth  19833  pilem3  19845  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  logltb  19969  logcnlem5  20009  cxpcn3lem  20103  cxpcn3  20104  cxpaddle  20108  logreclem  20132  rlimcnp  20276  rlimcnp2  20277  xrlimcnp  20279  rlimcxp  20284  cxploglim  20288  jensen  20299  emcllem6  20310  emcllem7  20311  ftalem2  20327  ftalem3  20328  ftalem5  20330  sqfpc  20391  mumullem2  20434  sqff1o  20436  chtublem  20466  chtub  20467  fsumvma2  20469  chpchtsum  20474  logexprlim  20480  bposlem6  20544  lgslem2  20552  lgslem3  20553  lgsval  20555  lgsfcl2  20557  lgsfle1  20560  lgsle1  20566  lgsdirprm  20584  chtppilimlem2  20639  chtppilim  20640  dchrisumlema  20653  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  dchrisum  20657  dchrmusumlema  20658  dchrvmasumlem2  20663  dchrisum0flblem1  20673  dchrisum0lema  20679  2vmadivsumlem  20705  chpdifbndlem1  20718  selberg3lem1  20722  selberg4lem1  20725  pntrsumbnd  20731  pntrsumbnd2  20732  selbergsb  20740  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd1  20751  pntpbnd2  20752  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemn  20765  pntlemj  20768  pntlemi  20769  pntlemo  20772  pntlem3  20774  pntlemp  20775  pntleml  20776  pnt3  20777  padicabv  20795  ostth2lem2  20799  ostth3  20803  ostth  20804  isnvlem  21182  nvelbl  21278  nvelbl2  21279  nmoofval  21356  nmosetn0  21359  nmoolb  21365  nmoubi  21366  nmounbseqi  21371  nmounbseqiOLD  21372  nmobndseqi  21373  nmobndseqiOLD  21374  bloval  21375  isblo  21376  nmoo0  21385  nmlno0lem  21387  blocnilem  21398  siilem2  21446  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  ubth  21468  minvecolem3  21471  minvecolem4  21475  minvecolem5  21476  minvecolem7  21478  htthlem  21513  htth  21514  h2hcau  21575  h2hlm  21576  normlem7tALT  21714  norm3lemt  21747  hcau  21779  hlimi  21783  hlim2  21787  cmcm3  22210  pjnorm  22319  pjnel  22321  elcnop  22453  elbdop  22456  nmopsetn0  22461  nmfnsetn0  22474  elcnfn  22478  hhcno  22500  hhcnf  22501  nmoplb  22503  nmopub  22504  cnopc  22509  nmfnlb  22520  nmfnleub  22521  cnfnc  22526  idcnop  22577  nmop0  22582  nmfn0  22583  nmlnop0iALT  22591  nmcexi  22622  nmcopexi  22623  lnconi  22629  lnopcon  22631  nmcfnexi  22647  lnfncon  22652  branmfn  22701  leop3  22721  opsqrlem6  22741  cvmd  22932  cvdmd  22933  cvexch  22970  cdj3i  23037  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemimin  23080  ballotlemic  23081  ballotlem1c  23082  ballotlemsv  23084  ballotlemfrcn0  23104  ballotlemrc  23105  xdivpnfrp  23133  fmptcof2  23244  xraddge02  23267  sqsscirc2  23308  cnre2csqlem  23309  xrge0iifiso  23332  lmdvg  23391  dya2ub  23590  erdszelem8  23744  kur14  23762  umgrale  23888  umgrafi  23889  umgra1  23893  umgrabi  23922  snmlval  23929  snmlflim  23930  sinccvg  24021  abs2sqle  24031  abs2sqlt  24032  cprodeq1f  24130  cprodeq2w  24134  cprodeq2ii  24135  prodrblem2  24154  prodmolem2  24158  prodmo  24159  zprod  24160  zprodn0  24162  poseq  24324  soseq  24325  sltval  24372  brimg  24547  brbtwn2  24605  colinearalg  24610  axcontlem10  24673  cgrtriv  24697  cgrdegen  24699  brofs  24700  cgrextend  24703  segconeu  24706  fvtransport  24727  transportprops  24729  brifs  24738  ifscgr  24739  brcgr3  24741  cgrxfr  24750  brfs  24774  btwnconn1lem7  24788  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn1lem14  24795  brsegle  24803  segleantisym  24810  outsideofeu  24826  nndivlub  24969  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  bddiblnc  25021  ftc1cnnclem  25024  ftc1cnnc  25025  areacirclem2  25028  areacirclem3  25029  areacirclem4  25030  areacirclem5  25032  areacirclem6  25033  areacirc  25034  oriso  25317  mslb1  25710  nn0prpwlem  26341  nn0prpw  26342  seqpo  26560  incsequz2  26562  lmclim2  26577  geomcau  26578  caushft  26580  prdsbnd  26620  ismtyima  26630  heiborlem4  26641  heiborlem6  26643  heiborlem7  26644  bfplem1  26649  bfplem2  26650  rrndstprj2  26658  rrncmslem  26659  rrnequiv  26662  irrapxlem3  27012  irrapxlem4  27013  irrapxlem5  27014  irrapxlem6  27015  pellexlem3  27019  monotoddzz  27131  jm2.19  27189  rmydioph  27210  fnwe2lem2  27251  islinds  27382  lindsss  27397  hbtlem1  27430  hbtlem2  27431  hbtlem7  27432  hbtlem4  27433  hbtlem5  27435  hbtlem6  27436  dgrsub2  27442  symggen  27514  fiuneneq  27616  evth2f  27789  evthf  27801  cncmpmax  27806  rfcnpre4  27808  fmul01  27813  climinf  27835  climsuse  27837  stoweidlem7  27859  stoweidlem9  27861  stoweidlem15  27867  stoweidlem16  27868  stoweidlem18  27870  stoweidlem21  27873  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem36  27888  stoweidlem37  27889  stoweidlem41  27893  stoweidlem44  27896  stoweidlem45  27897  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem55  27907  stoweidlem59  27911  stoweidlem60  27912  hashgt12el2  28219  uslgra1  28252  oposlem  29995  opltcon2b  30018  pats  30097  ishlat1  30164  cvrexch  30231  atle  30247  athgt  30267  1cvrco  30283  3atlem5  30298  4atlem3  30407  dalawlem15  30696  lhprelat3N  30851  lautle  30895  lautcvr  30903  ltrnatb  30948  ltrneq2  30959  cdlemefr32sn2aw  31215  cdlemefs32sn1aw  31225  cdleme32fvaw  31250  cdleme35sn3a  31270  cdleme46frvlpq  31315  cdleme48gfv  31348  trlord  31380  cdlemg1fvawlemN  31384  cdlemg7fvbwN  31418  cdlemg31d  31511  istendo  31571  dva1dim  31796  dvhb1dimN  31797  diafval  31843  diaelval  31845  cdlemm10N  31930  dihopelvalcpre  32060  dihmeetcN  32114  dihmeetlem6  32121  dihjatc1  32123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator