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

Theorem breq1d 4447
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 4440 . 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 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  eqbrtrd  4457  syl6eqbr  4474  sbcbr2g  4493  pofun  4806  dffv2  5931  fmptco  6049  isorel  6207  soisores  6208  soisoi  6209  isocnv  6211  isotr  6217  f1owe  6234  weniso  6235  caovordig  6465  caovordg  6467  caovord  6471  f1oweALT  6769  frxp  6895  xporderlem  6896  fnwelem  6900  reldmtpos  6965  brtpos  6966  tpostpos  6977  tposoprab  6993  ensn1g  7582  fndmeng  7594  xpsneng  7604  xpcomco  7609  pwdom  7671  snnen2o  7708  supgtoreq  7931  ordtypelem6  7951  ordtypelem7  7952  wdompwdom  8007  infdiffi  8077  r1sdom  8195  pm54.43  8384  prdom2  8387  indcardi  8425  alephordi  8458  cdalepw  8579  fin23lem26  8708  fin23lem23  8709  fin23lem22  8710  fin23lem27  8711  uniimadomf  8923  alephval2  8950  inar1  9156  nqereu  9310  ltrnq  9360  prlem934  9414  prlem936  9428  ltasr  9480  addgt0sr  9484  axpre-ltadd  9547  axpre-sup  9549  ltsubadd  10029  lesubadd  10031  ltaddsub2  10034  leaddsub2  10036  ltaddpos  10049  lesub2  10054  ltnegcon2  10061  lenegcon2  10064  addge01  10069  subge0  10072  suble0  10073  lesub0  10076  ltordlem  10085  mulgt1  10408  ltmulgt11  10409  gt0div  10415  ge0div  10416  ltmuldiv  10422  ltmuldiv2  10423  lemuldiv2  10432  ltrec  10433  lerec2  10440  ltdiv23  10443  lediv23  10444  addltmul  10781  avglt1  10783  avgle1  10785  avgle  10787  zlem1lt  10922  zgt0ge1  10924  rpnnen1lem5  11223  reexALT  11225  xrmin2  11390  xltnegi  11426  xmulval  11435  xlesubadd  11466  xmullem2  11468  nn0disj  11802  dfceil2  11950  uzenom  12057  seqf1olem1  12128  leexp2r  12205  sqlecan  12256  expmulnbnd  12280  hashbnd  12393  hashle00  12447  hashgt12el2  12464  hashf1  12488  seqcoll  12494  hashge3el3dif  12506  lswccatn0lsw  12589  swrdccatin2  12694  swrd2lsw  12872  2swrd2eqwrdeq  12873  shftfval  12885  shftfib  12887  shftfn  12888  2shfti  12895  shftidt2  12896  sqrlem1  13058  sqrlem2  13059  sqrlem6  13063  sqrlem7  13064  absdiflt  13132  absdifle  13133  lenegsq  13135  cau3lem  13169  limsupgle  13282  limsupgre  13286  clim  13299  rlim  13300  rlim2  13301  clim2  13309  clim0  13311  clim0c  13312  rlim0  13313  rlim0lt  13314  climi0  13317  ello1  13320  ello1mpt  13326  elo1  13331  lo1o1  13337  rlimclim1  13350  rlimclim  13351  climrlim2  13352  rlimuni  13355  climuni  13357  lo1res  13364  rlimresb  13370  rlimeq  13374  2clim  13377  climshftlem  13379  climshft  13381  climabs0  13390  o1co  13391  rlimcn1  13393  rlimcn2  13395  climcn1  13396  climcn2  13397  addcn2  13398  subcn2  13399  mulcn2  13400  o1of2  13417  o1rlimmul  13423  rlimdiv  13450  rlimno1  13458  isershft  13468  isercoll  13472  climsup  13474  climcau  13475  caucvgrlem  13477  caucvgrlem2  13479  caurcvg2  13482  caucvg  13483  caucvgb  13484  serf0  13485  iseraltlem2  13487  iseralt  13489  sumeq1  13493  sumeq2w  13496  sumeq2ii  13497  sumrb  13517  summolem2  13520  summo  13521  zsum  13522  o1fsum  13609  cvgcmp  13612  cvgcmpce  13614  isumshft  13633  climcndslem1  13643  geolim  13661  geolim2  13662  geoisum1c  13671  mertenslem1  13675  mertenslem2  13676  mertens  13677  ntrivcvg  13688  ntrivcvgn0  13689  ntrivcvgmullem  13692  prodeq1f  13697  prodeq2w  13701  prodeq2ii  13702  prodrblem2  13720  prodmolem2  13724  prodmo  13725  zprod  13726  fprodntriv  13731  sin01bnd  13902  cos01bnd  13903  rpnnen  13942  ruclem9  13953  ruclem12  13956  sadcaddlem  14089  gcddvds  14135  dvdssq  14180  isprm  14201  isprm2lem  14206  prmgt1  14218  prmn2uzge3  14219  isprm6  14232  isprm5  14235  odzdvds  14304  pclem  14344  pcprecl  14345  pcprendvds  14346  pcpremul  14349  pcval  14350  pceulem  14351  pczndvds  14370  pcelnn  14375  pc2dvds  14384  pcadd  14390  pcadd2  14391  pcmpt  14393  prmpwdvds  14404  prmreclem1  14416  prmreclem5  14420  prmreclem6  14421  4sqlem17  14461  vdwlem10  14490  ramval  14508  0ram  14520  ram0  14522  ramz2  14524  ramub1lem2  14527  imasaddfnlem  14907  imasvscafn  14916  imasleval  14920  mreexexlemd  15023  symggen  16474  oddvdsnn0  16547  oddvds  16550  odf1  16563  odf1o1  16571  odf1o2  16572  gexdvds  16583  sylow1lem3  16599  efginvrel2  16724  efgsfo  16736  efgredlemd  16741  efgredlem  16744  efgred  16745  gexexlem  16837  torsubg  16839  oddvdssubg  16840  lt6abl  16876  ablfacrplem  17095  ablfacrp  17096  ablfaclem3  17117  abvfval  17446  abvpropd  17470  evlslem2  18159  znf1o  18568  znidomb  18578  cygznlem1  18583  frlmup1  18810  islinds  18822  lindsss  18837  chfacfscmul0  19337  chfacfscmulfsupp  19338  chfacfpmmul0  19341  chfacfpmmulfsupp  19342  cayleyhamilton1  19371  cctop  19485  ordthmeolem  20280  csdfil  20373  ufilen  20409  ptcmplem2  20531  ptcmplem3  20532  cnextfvval  20543  prdsxmetlem  20849  blfvalps  20864  elblps  20868  elbl  20869  elbl3ps  20872  elbl3  20873  blres  20912  imasf1obl  20969  blcld  20986  comet  20994  stdbdmetval  20995  stdbdbl  20998  metcnp2  21023  txmetcnp  21028  dscopn  21072  ngptgp  21128  nlmvscn  21174  nrginvrcn  21178  nmoval  21200  nghmcn  21230  cnbl0  21259  cnblcld  21260  bl2ioo  21275  recld2  21297  icccmplem2  21306  addcnlem  21346  divcn  21350  elcncf  21371  elcncf2  21372  cncfi  21376  rescncf  21379  mulc1cncf  21387  cncfco  21389  cncfmet  21390  cnheiborlem  21432  cnheibor  21433  cnllycmp  21434  evth  21437  htpycc  21458  phtpycc  21469  pcohtpylem  21497  pcoass  21502  pcorevlem  21504  nmoleub2lem2  21577  nmoleub3  21580  nmhmcn  21581  ipcau2  21655  ipcn  21664  lmmbr2  21676  lmmcvg  21678  lmmbrf  21679  fmcfil  21689  iscau2  21694  iscau4  21696  iscauf  21697  caucfil  21700  iscmet3lem3  21707  iscmet3lem1  21708  iscmet3lem2  21709  cfilresi  21712  cfilres  21713  caussi  21714  causs  21715  lmle  21718  lmclim  21719  bcthlem1  21741  bcthlem4  21744  bcth  21746  minveclem3b  21821  minveclem3  21822  minveclem4  21825  minveclem5  21826  minveclem7  21828  pmltpclem1  21838  pmltpc  21840  ivthlem1  21841  ivthlem2  21842  ivthlem3  21843  ivth  21844  cniccbdd  21851  ovolunlem1  21886  ovoliunlem1  21891  ovoliunlem2  21892  ovoliunlem3  21893  ovolshftlem1  21898  ovolscalem1  21902  ovolicc1  21905  ovolicc2lem3  21908  ovolicc2lem4  21909  ovolicc2lem5  21910  ioombl1lem4  21949  ioombl1  21950  uniioombllem6  21975  volsup2  21992  volcn  21993  mbfmulc2lem  22032  mbfsup  22049  mbflimsup  22051  itg1climres  22099  mbfi1fseqlem6  22105  mbfi1fseq  22106  mbfi1flimlem  22107  itg2leub  22119  itg2seq  22127  itg2mulclem  22131  itg2monolem1  22135  itg2mono  22138  itg2i1fseq  22140  itg2addlem  22143  itg2gt0  22145  itg2cnlem1  22146  itg2cnlem2  22147  itg2cn  22148  bddmulibl  22223  itgcn  22227  ellimc3  22261  dveflem  22358  dvferm1lem  22363  dvferm2lem  22365  rolle  22369  dvlip  22372  dvlipcn  22373  dvlip2  22374  c1liplem1  22375  c1lip3  22378  dvge0  22385  dvivthlem1  22387  lhop1lem  22392  lhop1  22393  dvcvx  22399  dvfsumabs  22402  dvfsumlem2  22406  dvfsumrlim  22410  ftc1a  22416  ftc1lem4  22418  ftc1lem6  22420  itgsubstlem  22427  mdegleb  22442  mdegmullem  22456  deg1lt0  22469  ply1divmo  22514  ply1divex  22515  ply1divalg2  22517  q1peqb  22533  fta1g  22546  dgrub  22609  coe1termlem  22633  dgrcolem2  22649  dgrco  22650  quotval  22666  plydivlem3  22669  plydivlem4  22670  plydivex  22671  plydivalg  22673  quotlem  22674  plyrem  22679  fta1  22682  aannenlem1  22702  aannenlem2  22703  aalioulem3  22708  aalioulem4  22709  aalioulem5  22710  aalioulem6  22711  aaliou  22712  aaliou2  22714  aaliou2b  22715  ulmval  22753  ulm2  22758  ulmclm  22760  ulmshftlem  22762  ulmcaulem  22767  ulmcau  22768  ulmss  22770  ulmcn  22772  ulmdvlem1  22773  ulmdvlem3  22775  mtestbdd  22778  iblulm  22780  itgulm  22781  radcnvlem1  22786  pserulm  22795  abelthlem2  22805  abelthlem5  22808  abelthlem7  22811  abelthlem8  22812  abelthlem9  22813  abelth  22814  pilem3  22826  sincosq2sgn  22870  sincosq3sgn  22871  sincosq4sgn  22872  logltb  22962  logcnlem5  23005  cxpcn3lem  23099  cxpcn3  23100  cxpaddle  23104  logreclem  23128  rlimcnp  23273  rlimcnp2  23274  xrlimcnp  23276  rlimcxp  23281  cxploglim  23285  jensen  23296  emcllem6  23308  emcllem7  23309  ftalem2  23325  ftalem3  23326  ftalem5  23328  sqfpc  23389  mumullem2  23432  sqff1o  23434  chtublem  23464  chtub  23465  fsumvma2  23467  chpchtsum  23472  logexprlim  23478  bposlem6  23542  lgslem2  23550  lgslem3  23551  lgsval  23553  lgsfcl2  23555  lgsfle1  23558  lgsle1  23564  lgsdirprm  23582  chtppilimlem2  23637  chtppilim  23638  dchrisumlema  23651  dchrisumlem1  23652  dchrisumlem2  23653  dchrisumlem3  23654  dchrisum  23655  dchrmusumlema  23656  dchrvmasumlem2  23661  dchrisum0flblem1  23671  dchrisum0lema  23677  2vmadivsumlem  23703  chpdifbndlem1  23716  selberg3lem1  23720  selberg4lem1  23723  pntrsumbnd  23729  pntrsumbnd2  23730  selbergsb  23738  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntpbnd1  23749  pntpbnd2  23750  pntibndlem2  23754  pntibndlem3  23755  pntibnd  23756  pntlemn  23763  pntlemj  23766  pntlemi  23767  pntlemo  23770  pntlem3  23772  pntlemp  23773  pntleml  23774  pnt3  23775  padicabv  23793  ostth2lem2  23797  ostth3  23801  ostth  23802  mirbtwnhl  24038  foot  24074  footeq  24076  mideulem2  24086  opphllem6  24102  hpgbr  24107  lmieu  24128  iscgra  24147  brbtwn2  24186  colinearalg  24191  axcontlem10  24254  umgrale  24299  umgrafi  24300  umgra1  24304  uslgra1  24350  1pthoncl  24572  2pthoncl  24583  clwlkisclwwlk2  24768  0eusgraiff0rgra  24917  umgrabi  24961  frgrawopreglem2  25023  isnvlem  25481  nvelbl  25577  nvelbl2  25578  nmoofval  25655  nmosetn0  25658  nmoolb  25664  nmoubi  25665  nmounbseqi  25670  nmounbseqiOLD  25671  nmobndseqi  25672  nmobndseqiOLD  25673  bloval  25674  isblo  25675  nmoo0  25684  nmlno0lem  25686  blocnilem  25697  siilem2  25745  ubthlem1  25764  ubthlem2  25765  ubthlem3  25766  ubth  25767  minvecolem3  25770  minvecolem4  25774  minvecolem5  25775  minvecolem7  25777  htthlem  25812  htth  25813  h2hcau  25874  h2hlm  25875  normlem7tALT  26014  norm3lemt  26047  hcau  26079  hlimi  26083  hlim2  26087  cmcm3  26511  pjnorm  26620  pjnel  26622  elcnop  26754  elbdop  26757  nmopsetn0  26762  nmfnsetn0  26775  elcnfn  26779  hhcno  26801  hhcnf  26802  nmoplb  26804  nmopub  26805  cnopc  26810  nmfnlb  26821  nmfnleub  26822  cnfnc  26827  idcnop  26878  nmop0  26883  nmfn0  26884  nmlnop0iALT  26892  nmcexi  26923  nmcopexi  26924  lnconi  26930  lnopcon  26932  nmcfnexi  26948  lnfncon  26953  branmfn  27002  leop3  27022  opsqrlem6  27042  cvmd  27233  cvdmd  27234  cvexch  27271  cdj3i  27338  fmptcof2  27480  xraddge02  27555  xdivpnfrp  27607  omndadd  27674  omndmul  27682  archirngz  27711  archiabllem2a  27716  isorng  27767  locfinreflem  27821  locfinref  27822  sqsscirc2  27869  cnre2csqlem  27870  xrge0iifiso  27895  lmdvg  27913  qqhcn  27950  qqhucn  27951  brfae  28198  dya2ub  28219  oddpwdc  28271  eulerpartlemd  28283  ballotlemfc0  28409  ballotlemfcc  28410  ballotlemimin  28422  ballotlemic  28423  ballotlemsv  28426  ballotlemfrcn0  28446  ballotlemrc  28447  sgnmul  28459  sgnmulsgn  28466  signsply0  28486  signswch  28496  signsvfn  28517  signsvfnn  28521  signlem0  28522  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem5  28553  lgamgulmlem6  28554  lgambdd  28557  lgamucov  28558  lgamcvglem  28560  erdszelem8  28620  kur14  28638  snmlval  28754  snmlflim  28755  sinccvg  29017  abs2sqle  29024  abs2sqlt  29025  faclim2  29149  poseq  29309  soseq  29310  sltval  29383  brimg  29563  cgrtriv  29628  cgrdegen  29630  brofs  29631  cgrextend  29634  segconeu  29637  fvtransport  29658  transportprops  29660  brifs  29669  ifscgr  29670  brcgr3  29672  cgrxfr  29681  brfs  29705  btwnconn1lem7  29719  btwnconn1lem11  29723  btwnconn1lem12  29724  btwnconn1lem14  29726  brsegle  29734  segleantisym  29741  outsideofeu  29757  nndivlub  29899  heicant  30025  dvtanlem  30040  itg2addnclem  30042  itg2addnclem3  30044  itg2addnc  30045  itg2gt0cn  30046  bddiblnc  30061  ftc1cnnclem  30064  ftc1cnnc  30065  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anc  30074  areacirclem1  30083  areacirclem2  30084  areacirclem4  30086  areacirclem5  30087  areacirc  30088  nn0prpwlem  30116  nn0prpw  30117  seqpo  30216  incsequz2  30218  lmclim2  30227  geomcau  30228  caushft  30230  prdsbnd  30265  ismtyima  30275  heiborlem4  30286  heiborlem6  30288  heiborlem7  30289  bfplem1  30294  bfplem2  30295  rrndstprj2  30303  rrncmslem  30304  rrnequiv  30307  irrapxlem3  30736  irrapxlem4  30737  irrapxlem5  30738  irrapxlem6  30739  pellexlem3  30743  monotoddzz  30855  jm2.19  30911  rmydioph  30932  fnwe2lem2  30973  hbtlem1  31048  hbtlem2  31049  hbtlem7  31050  hbtlem4  31051  hbtlem5  31053  hbtlem6  31054  dgrsub2  31060  fiuneneq  31130  isprm7  31168  lcmgcdlem  31188  lcmdvds  31190  nzss  31198  evth2f  31344  evthf  31356  cncmpmax  31361  rfcnpre4  31363  fmul01  31528  climinf  31566  climsuse  31568  mullimc  31576  ellimcabssub0  31577  climf  31582  mullimcf  31583  idlimc  31586  limcperiod  31588  clim2f  31596  limsupre  31601  limcleqr  31604  limclner  31611  clim0cf  31614  cncfshift  31630  cncfperiod  31635  fperdvper  31669  dvbdfbdioolem2  31680  dvbdfbdioo  31681  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  stoweidlem7  31743  stoweidlem9  31745  stoweidlem15  31751  stoweidlem16  31752  stoweidlem18  31754  stoweidlem21  31757  stoweidlem26  31762  stoweidlem31  31767  stoweidlem34  31770  stoweidlem36  31772  stoweidlem37  31773  stoweidlem41  31777  stoweidlem44  31780  stoweidlem45  31781  stoweidlem46  31782  stoweidlem48  31784  stoweidlem51  31787  stoweidlem52  31788  stoweidlem55  31791  stoweidlem59  31795  stoweidlem60  31796  fourierdlem20  31863  fourierdlem25  31868  fourierdlem37  31880  fourierdlem39  31882  fourierdlem41  31884  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem54  31897  fourierdlem64  31907  fourierdlem68  31911  fourierdlem70  31913  fourierdlem71  31914  fourierdlem73  31916  fourierdlem79  31922  fourierdlem80  31923  fourierdlem87  31930  fourierdlem96  31939  fourierdlem97  31940  fourierdlem98  31941  fourierdlem99  31942  fourierdlem103  31946  fourierdlem104  31947  fourierdlem105  31948  fourierdlem108  31951  fourierdlem109  31952  fourierdlem111  31954  fourierswlem  31967  fouriersw  31968  etransclem31  32002  etransclem47  32018  etransclem48  32019  etransc  32020  pgrpgt2nabl  32827  ply1mulgsumlem1  32856  ply1mulgsumlem2  32857  oposlem  34782  opltcon2b  34806  pats  34885  ishlat1  34952  cvrexch  35019  atle  35035  athgt  35055  1cvrco  35071  3atlem5  35086  4atlem3  35195  dalawlem15  35484  lhprelat3N  35639  lautle  35683  lautcvr  35691  ltrnatb  35736  ltrneq2  35747  cdlemefr32sn2aw  36005  cdlemefs32sn1aw  36015  cdleme32fvaw  36040  cdleme35sn3a  36060  cdleme46frvlpq  36105  cdleme48gfv  36138  trlord  36170  cdlemg1fvawlemN  36174  cdlemg7fvbwN  36208  cdlemg31d  36301  istendo  36361  dva1dim  36586  dvhb1dimN  36587  diafval  36633  diaelval  36635  cdlemm10N  36720  dihopelvalcpre  36850  dihmeetcN  36904  dihmeetlem6  36911  dihjatc1  36913  rp-isfinite5  37581  leeq1d  37773  extoimad  37785
  Copyright terms: Public domain W3C validator