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

Theorem breq1d 4457
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 4450 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  eqbrtrd  4467  syl6eqbr  4484  sbcbr2g  4503  pofun  4816  dffv2  5938  fmptco  6052  isorel  6208  soisores  6209  soisoi  6210  isocnv  6212  isotr  6218  f1owe  6235  weniso  6236  caovordig  6462  caovordg  6464  caovord  6468  f1oweALT  6765  frxp  6890  xporderlem  6891  fnwelem  6895  reldmtpos  6960  brtpos  6961  tpostpos  6972  tposoprab  6988  ensn1g  7577  fndmeng  7589  xpsneng  7599  xpcomco  7604  pwdom  7666  snnen2o  7703  supgtoreq  7924  ordtypelem6  7944  ordtypelem7  7945  wdompwdom  8000  infdiffi  8070  r1sdom  8188  pm54.43  8377  prdom2  8380  indcardi  8418  alephordi  8451  cdalepw  8572  fin23lem26  8701  fin23lem23  8702  fin23lem22  8703  fin23lem27  8704  uniimadomf  8916  alephval2  8943  inar1  9149  nqereu  9303  ltrnq  9353  prlem934  9407  prlem936  9421  ltasr  9473  addgt0sr  9477  axpre-ltadd  9540  axpre-sup  9542  ltsubadd  10018  lesubadd  10020  ltaddsub2  10023  leaddsub2  10025  ltaddpos  10038  lesub2  10043  ltnegcon2  10050  lenegcon2  10053  addge01  10058  subge0  10061  suble0  10062  lesub0  10065  ltordlem  10074  mulgt1  10397  ltmulgt11  10398  gt0div  10404  ge0div  10405  ltmuldiv  10411  ltmuldiv2  10412  lemuldiv2  10421  ltrec  10422  lerec2  10429  ltdiv23  10432  lediv23  10433  addltmul  10770  avglt1  10772  avgle1  10774  avgle  10776  zlem1lt  10910  zgt0ge1  10912  rpnnen1lem5  11208  reexALT  11210  xrmin2  11375  xltnegi  11411  xmulval  11420  xlesubadd  11451  xmullem2  11453  nn0disj  11784  dfceil2  11931  uzenom  12038  seqf1olem1  12109  leexp2r  12185  sqlecan  12236  expmulnbnd  12260  hashbnd  12373  hashle00  12425  hashgt12el2  12441  hashf1  12466  seqcoll  12472  hashge3el3dif  12484  lswccatn0lsw  12565  swrdccatin2  12669  swrd2lsw  12847  2swrd2eqwrdeq  12848  shftfval  12860  shftfib  12862  shftfn  12863  2shfti  12870  shftidt2  12871  sqrlem1  13033  sqrlem2  13034  sqrlem6  13038  sqrlem7  13039  absdiflt  13106  absdifle  13107  lenegsq  13109  cau3lem  13143  limsupgle  13256  limsupgre  13260  clim  13273  rlim  13274  rlim2  13275  clim2  13283  clim0  13285  clim0c  13286  rlim0  13287  rlim0lt  13288  climi0  13291  ello1  13294  ello1mpt  13300  elo1  13305  lo1o1  13311  rlimclim1  13324  rlimclim  13325  climrlim2  13326  rlimuni  13329  climuni  13331  lo1res  13338  rlimresb  13344  rlimeq  13348  2clim  13351  climshftlem  13353  climshft  13355  climabs0  13364  o1co  13365  rlimcn1  13367  rlimcn2  13369  climcn1  13370  climcn2  13371  addcn2  13372  subcn2  13373  mulcn2  13374  o1of2  13391  o1rlimmul  13397  rlimdiv  13424  rlimno1  13432  isershft  13442  isercoll  13446  climsup  13448  climcau  13449  caucvgrlem  13451  caucvgrlem2  13453  caurcvg2  13456  caucvg  13457  caucvgb  13458  serf0  13459  iseraltlem2  13461  iseralt  13463  sumeq1  13467  sumeq2w  13470  sumeq2ii  13471  sumrb  13491  summolem2  13494  summo  13495  zsum  13496  o1fsum  13583  cvgcmp  13586  cvgcmpce  13588  isumshft  13607  climcndslem1  13617  geolim  13635  geolim2  13636  geoisum1c  13645  mertenslem1  13649  mertenslem2  13650  mertens  13651  sin01bnd  13774  cos01bnd  13775  rpnnen  13814  ruclem9  13825  ruclem12  13828  sadcaddlem  13959  gcddvds  14005  dvdssq  14050  isprm  14071  isprm2lem  14076  prmgt1  14088  prmn2uzge3  14089  isprm6  14102  isprm5  14105  odzdvds  14174  pclem  14214  pcprecl  14215  pcprendvds  14216  pcpremul  14219  pcval  14220  pceulem  14221  pczndvds  14240  pcelnn  14245  pc2dvds  14254  pcadd  14260  pcadd2  14261  pcmpt  14263  prmpwdvds  14274  prmreclem1  14286  prmreclem5  14290  prmreclem6  14291  4sqlem17  14331  vdwlem10  14360  ramval  14378  0ram  14390  ram0  14392  ramz2  14394  ramub1lem2  14397  imasaddfnlem  14776  imasvscafn  14785  imasleval  14789  mreexexlemd  14892  symggen  16288  oddvdsnn0  16361  oddvds  16364  odf1  16377  odf1o1  16385  odf1o2  16386  gexdvds  16397  sylow1lem3  16413  efginvrel2  16538  efgsfo  16550  efgredlemd  16555  efgredlem  16558  efgred  16559  gexexlem  16648  torsubg  16650  oddvdssubg  16651  lt6abl  16685  ablfacrplem  16903  ablfacrp  16904  ablfaclem3  16925  abvfval  17247  abvpropd  17271  mptscmfsuppd  17357  evlslem2  17948  znf1o  18354  znidomb  18364  cygznlem1  18369  frlmup1  18596  islinds  18608  lindsss  18623  chfacfscmul0  19123  chfacfscmulfsupp  19124  chfacfpmmul0  19127  chfacfpmmulfsupp  19128  cayleyhamilton1  19157  cctop  19270  ordthmeolem  20034  csdfil  20127  ufilen  20163  ptcmplem2  20285  ptcmplem3  20286  cnextfvval  20297  prdsxmetlem  20603  blfvalps  20618  elblps  20622  elbl  20623  elbl3ps  20626  elbl3  20627  blres  20666  imasf1obl  20723  blcld  20740  comet  20748  stdbdmetval  20749  stdbdbl  20752  metcnp2  20777  txmetcnp  20782  dscopn  20826  ngptgp  20882  nlmvscn  20928  nrginvrcn  20932  nmoval  20954  nghmcn  20984  cnbl0  21013  cnblcld  21014  bl2ioo  21029  recld2  21051  icccmplem2  21060  addcnlem  21100  divcn  21104  elcncf  21125  elcncf2  21126  cncfi  21130  rescncf  21133  mulc1cncf  21141  cncfco  21143  cncfmet  21144  cnheiborlem  21186  cnheibor  21187  cnllycmp  21188  evth  21191  htpycc  21212  phtpycc  21223  pcohtpylem  21251  pcoass  21256  pcorevlem  21258  nmoleub2lem2  21331  nmoleub3  21334  nmhmcn  21335  ipcau2  21409  ipcn  21418  lmmbr2  21430  lmmcvg  21432  lmmbrf  21433  fmcfil  21443  iscau2  21448  iscau4  21450  iscauf  21451  caucfil  21454  iscmet3lem3  21461  iscmet3lem1  21462  iscmet3lem2  21463  cfilresi  21466  cfilres  21467  caussi  21468  causs  21469  lmle  21472  lmclim  21473  bcthlem1  21495  bcthlem4  21498  bcth  21500  minveclem3b  21575  minveclem3  21576  minveclem4  21579  minveclem5  21580  minveclem7  21582  pmltpclem1  21592  pmltpc  21594  ivthlem1  21595  ivthlem2  21596  ivthlem3  21597  ivth  21598  cniccbdd  21605  ovolunlem1  21640  ovoliunlem1  21645  ovoliunlem2  21646  ovoliunlem3  21647  ovolshftlem1  21652  ovolscalem1  21656  ovolicc1  21659  ovolicc2lem3  21662  ovolicc2lem4  21663  ovolicc2lem5  21664  ioombl1lem4  21703  ioombl1  21704  uniioombllem6  21729  volsup2  21746  volcn  21747  mbfmulc2lem  21786  mbfsup  21803  mbflimsup  21805  itg1climres  21853  mbfi1fseqlem6  21859  mbfi1fseq  21860  mbfi1flimlem  21861  itg2leub  21873  itg2seq  21881  itg2mulclem  21885  itg2monolem1  21889  itg2mono  21892  itg2i1fseq  21894  itg2addlem  21897  itg2gt0  21899  itg2cnlem1  21900  itg2cnlem2  21901  itg2cn  21902  bddmulibl  21977  itgcn  21981  ellimc3  22015  dveflem  22112  dvferm1lem  22117  dvferm2lem  22119  rolle  22123  dvlip  22126  dvlipcn  22127  dvlip2  22128  c1liplem1  22129  c1lip3  22132  dvge0  22139  dvivthlem1  22141  lhop1lem  22146  lhop1  22147  dvcvx  22153  dvfsumabs  22156  dvfsumlem2  22160  dvfsumrlim  22164  ftc1a  22170  ftc1lem4  22172  ftc1lem6  22174  itgsubstlem  22181  mdegleb  22196  mdegmullem  22210  deg1lt0  22223  ply1divmo  22268  ply1divex  22269  ply1divalg2  22271  q1peqb  22287  fta1g  22300  dgrub  22363  coe1termlem  22386  dgrcolem2  22402  dgrco  22403  quotval  22419  plydivlem3  22422  plydivlem4  22423  plydivex  22424  plydivalg  22426  quotlem  22427  plyrem  22432  fta1  22435  aannenlem1  22455  aannenlem2  22456  aalioulem3  22461  aalioulem4  22462  aalioulem5  22463  aalioulem6  22464  aaliou  22465  aaliou2  22467  aaliou2b  22468  ulmval  22506  ulm2  22511  ulmclm  22513  ulmshftlem  22515  ulmcaulem  22520  ulmcau  22521  ulmss  22523  ulmcn  22525  ulmdvlem1  22526  ulmdvlem3  22528  mtestbdd  22531  iblulm  22533  itgulm  22534  radcnvlem1  22539  pserulm  22548  abelthlem2  22558  abelthlem5  22561  abelthlem7  22564  abelthlem8  22565  abelthlem9  22566  abelth  22567  pilem3  22579  sincosq2sgn  22622  sincosq3sgn  22623  sincosq4sgn  22624  logltb  22709  logcnlem5  22752  cxpcn3lem  22846  cxpcn3  22847  cxpaddle  22851  logreclem  22875  rlimcnp  23020  rlimcnp2  23021  xrlimcnp  23023  rlimcxp  23028  cxploglim  23032  jensen  23043  emcllem6  23055  emcllem7  23056  ftalem2  23072  ftalem3  23073  ftalem5  23075  sqfpc  23136  mumullem2  23179  sqff1o  23181  chtublem  23211  chtub  23212  fsumvma2  23214  chpchtsum  23219  logexprlim  23225  bposlem6  23289  lgslem2  23297  lgslem3  23298  lgsval  23300  lgsfcl2  23302  lgsfle1  23305  lgsle1  23311  lgsdirprm  23329  chtppilimlem2  23384  chtppilim  23385  dchrisumlema  23398  dchrisumlem1  23399  dchrisumlem2  23400  dchrisumlem3  23401  dchrisum  23402  dchrmusumlema  23403  dchrvmasumlem2  23408  dchrisum0flblem1  23418  dchrisum0lema  23424  2vmadivsumlem  23450  chpdifbndlem1  23463  selberg3lem1  23467  selberg4lem1  23470  pntrsumbnd  23476  pntrsumbnd2  23477  selbergsb  23485  pntrlog2bndlem3  23489  pntrlog2bndlem5  23491  pntrlog2bndlem6  23493  pntpbnd1  23496  pntpbnd2  23497  pntibndlem2  23501  pntibndlem3  23502  pntibnd  23503  pntlemn  23510  pntlemj  23513  pntlemi  23514  pntlemo  23517  pntlem3  23519  pntlemp  23520  pntleml  23521  pnt3  23522  padicabv  23540  ostth2lem2  23544  ostth3  23548  ostth  23549  nehash2  23624  foot  23801  mideulem  23810  lmieu  23824  brbtwn2  23881  colinearalg  23886  axcontlem10  23949  umgrale  23994  umgrafi  23995  umgra1  23999  uslgra1  24045  1pthoncl  24267  2pthoncl  24278  clwlkisclwwlk2  24463  0eusgraiff0rgra  24612  umgrabi  24656  frgrawopreglem2  24719  isnvlem  25176  nvelbl  25272  nvelbl2  25273  nmoofval  25350  nmosetn0  25353  nmoolb  25359  nmoubi  25360  nmounbseqi  25365  nmounbseqiOLD  25366  nmobndseqi  25367  nmobndseqiOLD  25368  bloval  25369  isblo  25370  nmoo0  25379  nmlno0lem  25381  blocnilem  25392  siilem2  25440  ubthlem1  25459  ubthlem2  25460  ubthlem3  25461  ubth  25462  minvecolem3  25465  minvecolem4  25469  minvecolem5  25470  minvecolem7  25472  htthlem  25507  htth  25508  h2hcau  25569  h2hlm  25570  normlem7tALT  25709  norm3lemt  25742  hcau  25774  hlimi  25778  hlim2  25782  cmcm3  26206  pjnorm  26315  pjnel  26317  elcnop  26449  elbdop  26452  nmopsetn0  26457  nmfnsetn0  26470  elcnfn  26474  hhcno  26496  hhcnf  26497  nmoplb  26499  nmopub  26500  cnopc  26505  nmfnlb  26516  nmfnleub  26517  cnfnc  26522  idcnop  26573  nmop0  26578  nmfn0  26579  nmlnop0iALT  26587  nmcexi  26618  nmcopexi  26619  lnconi  26625  lnopcon  26627  nmcfnexi  26643  lnfncon  26648  branmfn  26697  leop3  26717  opsqrlem6  26737  cvmd  26928  cvdmd  26929  cvexch  26966  cdj3i  27033  fmptcof2  27171  xraddge02  27242  xdivpnfrp  27294  omndadd  27355  omndmul  27363  archirngz  27392  archiabllem2a  27397  isorng  27449  sqsscirc2  27524  cnre2csqlem  27525  xrge0iifiso  27550  lmdvg  27568  qqhcn  27605  qqhucn  27606  brfae  27857  dya2ub  27878  oddpwdc  27930  eulerpartlemd  27942  ballotlemfc0  28068  ballotlemfcc  28069  ballotlemimin  28081  ballotlemic  28082  ballotlemsv  28085  ballotlemfrcn0  28105  ballotlemrc  28106  sgnmul  28118  sgnmulsgn  28125  signsplypnf  28144  signsply0  28145  signswch  28155  signsvfn  28176  signsvfnn  28180  signlem0  28181  lgamgulmlem2  28209  lgamgulmlem3  28210  lgamgulmlem5  28212  lgamgulmlem6  28213  lgambdd  28216  lgamucov  28217  lgamcvglem  28219  erdszelem8  28279  kur14  28297  snmlval  28413  snmlflim  28414  sinccvg  28511  abs2sqle  28518  abs2sqlt  28519  ntrivcvg  28605  ntrivcvgn0  28606  ntrivcvgmullem  28609  prodeq1f  28614  prodeq2w  28618  prodeq2ii  28619  prodrblem2  28637  prodmolem2  28641  prodmo  28642  zprod  28643  fprodntriv  28648  faclim2  28747  poseq  28907  soseq  28908  sltval  28981  brimg  29161  cgrtriv  29226  cgrdegen  29228  brofs  29229  cgrextend  29232  segconeu  29235  fvtransport  29256  transportprops  29258  brifs  29267  ifscgr  29268  brcgr3  29270  cgrxfr  29279  brfs  29303  btwnconn1lem7  29317  btwnconn1lem11  29321  btwnconn1lem12  29322  btwnconn1lem14  29324  brsegle  29332  segleantisym  29339  outsideofeu  29355  nndivlub  29497  heicant  29624  dvtanlem  29639  itg2addnclem  29641  itg2addnclem3  29643  itg2addnc  29644  itg2gt0cn  29645  bddiblnc  29660  ftc1cnnclem  29663  ftc1cnnc  29664  ftc1anclem5  29669  ftc1anclem6  29670  ftc1anc  29673  areacirclem1  29682  areacirclem2  29683  areacirclem4  29685  areacirclem5  29686  areacirc  29687  nn0prpwlem  29715  nn0prpw  29716  seqpo  29841  incsequz2  29843  lmclim2  29852  geomcau  29853  caushft  29855  prdsbnd  29890  ismtyima  29900  heiborlem4  29911  heiborlem6  29913  heiborlem7  29914  bfplem1  29919  bfplem2  29920  rrndstprj2  29928  rrncmslem  29929  rrnequiv  29932  irrapxlem3  30362  irrapxlem4  30363  irrapxlem5  30364  irrapxlem6  30365  pellexlem3  30369  monotoddzz  30481  jm2.19  30539  rmydioph  30560  fnwe2lem2  30601  hbtlem1  30676  hbtlem2  30677  hbtlem7  30678  hbtlem4  30679  hbtlem5  30681  hbtlem6  30682  dgrsub2  30688  fiuneneq  30759  isprm7  30795  lcmgcdlem  30812  lcmdvds  30814  nzss  30822  evth2f  30968  evthf  30980  cncmpmax  30985  rfcnpre4  30987  fmul01  31130  climinf  31148  climsuse  31150  mullimc  31158  ellimcabssub0  31159  climf  31164  mullimcf  31165  idlimc  31168  limcperiod  31170  clim2f  31178  limsupre  31183  limcleqr  31186  limclner  31193  clim0cf  31196  cncfshift  31212  cncfperiod  31217  fperdvper  31248  dvbdfbdioolem2  31259  dvbdfbdioo  31260  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem7  31307  stoweidlem9  31309  stoweidlem15  31315  stoweidlem16  31316  stoweidlem18  31318  stoweidlem21  31321  stoweidlem26  31326  stoweidlem31  31331  stoweidlem34  31334  stoweidlem36  31336  stoweidlem37  31337  stoweidlem41  31341  stoweidlem44  31344  stoweidlem45  31345  stoweidlem46  31346  stoweidlem48  31348  stoweidlem51  31351  stoweidlem52  31352  stoweidlem55  31355  stoweidlem59  31359  stoweidlem60  31360  fourierdlem20  31427  fourierdlem25  31432  fourierdlem37  31444  fourierdlem39  31446  fourierdlem41  31448  fourierdlem45  31452  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem54  31461  fourierdlem64  31471  fourierdlem68  31475  fourierdlem70  31477  fourierdlem71  31478  fourierdlem73  31480  fourierdlem79  31486  fourierdlem80  31487  fourierdlem82  31489  fourierdlem87  31494  fourierdlem93  31500  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem103  31510  fourierdlem104  31511  fourierdlem105  31512  fourierdlem108  31515  fourierdlem109  31516  fourierdlem111  31518  fourierswlem  31531  fouriersw  31532  pgrpgt2nabl  32024  ply1mulgsumlem1  32059  ply1mulgsumlem2  32060  oposlem  33979  opltcon2b  34003  pats  34082  ishlat1  34149  cvrexch  34216  atle  34232  athgt  34252  1cvrco  34268  3atlem5  34283  4atlem3  34392  dalawlem15  34681  lhprelat3N  34836  lautle  34880  lautcvr  34888  ltrnatb  34933  ltrneq2  34944  cdlemefr32sn2aw  35200  cdlemefs32sn1aw  35210  cdleme32fvaw  35235  cdleme35sn3a  35255  cdleme46frvlpq  35300  cdleme48gfv  35333  trlord  35365  cdlemg1fvawlemN  35369  cdlemg7fvbwN  35403  cdlemg31d  35496  istendo  35556  dva1dim  35781  dvhb1dimN  35782  diafval  35828  diaelval  35830  cdlemm10N  35915  dihopelvalcpre  36045  dihmeetcN  36099  dihmeetlem6  36106  dihjatc1  36108
  Copyright terms: Public domain W3C validator