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

Theorem breq1d 4436
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 4429 . 2  |-  ( A  =  B  ->  ( A R C  <->  B R C ) )
31, 2syl 17 1  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   class class class wbr 4426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427
This theorem is referenced by:  eqbrtrd  4446  syl6eqbr  4463  sbcbr2g  4481  pofun  4791  dffv2  5954  fmptco  6071  isorel  6232  soisores  6233  soisoi  6234  isocnv  6236  isotr  6242  f1owe  6259  weniso  6260  caovordig  6488  caovordg  6490  caovord  6494  f1oweALT  6791  frxp  6917  xporderlem  6918  fnwelem  6922  reldmtpos  6989  brtpos  6990  tpostpos  7001  tposoprab  7017  ensn1g  7641  fndmeng  7653  xpsneng  7663  xpcomco  7668  pwdom  7730  snnen2o  7767  supgtoreq  7992  ordtypelem6  8038  ordtypelem7  8039  wdompwdom  8093  infdiffi  8162  r1sdom  8244  pm54.43  8433  prdom2  8436  indcardi  8470  alephordi  8503  cdalepw  8624  fin23lem26  8753  fin23lem23  8754  fin23lem22  8755  fin23lem27  8756  uniimadomf  8968  alephval2  8995  inar1  9199  nqereu  9353  ltrnq  9403  prlem934  9457  prlem936  9471  ltasr  9523  addgt0sr  9527  axpre-ltadd  9590  axpre-sup  9592  ltsubadd  10083  lesubadd  10085  ltaddsub2  10088  leaddsub2  10090  ltaddpos  10103  lesub2  10108  ltnegcon2  10115  lenegcon2  10118  addge01  10123  subge0  10126  suble0  10127  lesub0  10130  ltordlem  10138  mulgt1  10463  ltmulgt11  10464  gt0div  10470  ge0div  10471  ltmuldiv  10477  ltmuldiv2  10478  lemuldiv2  10486  ltrec  10487  lerec2  10494  ltdiv23  10497  lediv23  10498  addltmul  10848  avglt1  10850  avgle1  10852  avgle  10854  zlem1lt  10988  zgt0ge1  10990  rpnnen1lem5  11294  reexALT  11296  xrmin2  11473  xltnegi  11509  xmulval  11518  xlesubadd  11549  xmullem2  11551  nn0disj  11905  dfceil2  12065  uzenom  12175  seqf1olem1  12249  leexp2r  12327  sqlecan  12378  expmulnbnd  12401  hashbnd  12518  hashle00  12574  hashgt12el2  12591  hashf1  12615  seqcoll  12621  hashge3el3dif  12633  swrdccatin2  12828  swrd2lsw  13006  2swrd2eqwrdeq  13007  shftfval  13112  shftfib  13114  shftfn  13115  2shfti  13122  shftidt2  13123  sqrlem1  13285  sqrlem2  13286  sqrlem6  13290  sqrlem7  13291  absdiflt  13359  absdifle  13360  lenegsq  13362  cau3lem  13396  limsupgle  13513  limsupgre  13520  limsupgreOLD  13521  clim  13536  rlim  13537  rlim2  13538  clim2  13546  clim0  13548  clim0c  13549  rlim0  13550  rlim0lt  13551  climi0  13554  ello1  13557  ello1mpt  13563  elo1  13568  lo1o1  13574  rlimclim1  13587  rlimclim  13588  climrlim2  13589  rlimuni  13592  climuni  13594  lo1res  13601  rlimresb  13607  rlimeq  13611  2clim  13614  climshftlem  13616  climshft  13618  climabs0  13627  o1co  13628  rlimcn1  13630  rlimcn2  13632  climcn1  13633  climcn2  13634  addcn2  13635  subcn2  13636  mulcn2  13637  o1of2  13654  o1rlimmul  13660  rlimdiv  13687  rlimno1  13695  isershft  13705  isercoll  13709  climsup  13711  climcau  13712  caucvgrlem  13714  caucvgrlemOLD  13715  caucvgrlem2  13718  caurcvg2  13722  caucvg  13723  caucvgb  13724  serf0  13725  iseraltlem2  13727  iseralt  13729  sumeq1  13733  sumeq2w  13736  sumeq2ii  13737  sumrb  13757  summolem2  13760  summo  13761  zsum  13762  o1fsum  13851  cvgcmp  13854  cvgcmpce  13856  isumshft  13875  climcndslem1  13885  geolim  13904  geolim2  13905  geoisum1c  13914  mertenslem1  13918  mertenslem2  13919  mertens  13920  ntrivcvg  13931  ntrivcvgn0  13932  ntrivcvgmullem  13935  prodeq1f  13940  prodeq2w  13944  prodeq2ii  13945  prodrblem2  13963  prodmolem2  13967  prodmo  13968  zprod  13969  fprodntriv  13974  sin01bnd  14217  cos01bnd  14218  rpnnen  14257  ruclem9  14268  ruclem12  14271  sadcaddlem  14405  gcddvds  14451  dvdssq  14499  lcmgcdlem  14536  lcmdvds  14538  lcmfunsnlem  14576  isprm  14586  isprm2lem  14593  prmgt1  14605  prmn2uzge3  14606  isprm5  14613  isprm6  14628  coprmproddvdslem  14641  coprmproddvds  14642  odzdvds  14700  pclem  14742  pcprecl  14743  pcprendvds  14744  pcpremul  14747  pcval  14748  pceulem  14749  pczndvds  14768  pcelnn  14773  pc2dvds  14782  pcadd  14788  pcadd2  14789  pcmpt  14791  prmpwdvds  14802  prmreclem1  14814  prmreclem5  14818  prmreclem6  14819  4sqlem17OLD  14859  4sqlem17  14865  vdwlem10  14894  ramval  14914  ramvalOLD  14915  0ram  14932  ram0  14934  ramz2  14936  ramub1lem2  14939  imasaddfnlem  15376  imasvscafn  15385  imasleval  15389  mreexexlemd  15492  symggen  17053  oddvdsnn0  17126  oddvds  17129  odf1  17142  odf1o1  17150  odf1o2  17151  gexdvds  17162  sylow1lem3  17178  efginvrel2  17303  efgsfo  17315  efgredlemd  17320  efgredlem  17323  efgred  17324  gexexlem  17416  torsubg  17418  oddvdssubg  17419  lt6abl  17455  ablfacrplem  17624  ablfacrp  17625  ablfaclem3  17646  abvfval  17972  abvpropd  17996  evlslem2  18661  znf1o  19044  znidomb  19054  cygznlem1  19059  frlmup1  19278  islinds  19289  lindsss  19304  chfacfscmul0  19804  chfacfscmulfsupp  19805  chfacfpmmul0  19808  chfacfpmmulfsupp  19809  cayleyhamilton1  19838  cctop  19943  ordthmeolem  20738  csdfil  20831  ufilen  20867  ptcmplem2  20990  ptcmplem3  20991  cnextfvval  21002  prdsxmetlem  21305  blfvalps  21320  elblps  21324  elbl  21325  elbl3ps  21328  elbl3  21329  blres  21368  imasf1obl  21425  blcld  21442  comet  21450  stdbdmetval  21451  stdbdbl  21454  metcnp2  21479  txmetcnp  21484  dscopn  21510  ngptgp  21566  nlmvscn  21612  nrginvrcn  21616  nmoval  21638  nghmcn  21668  cnbl0  21696  cnblcld  21697  bl2ioo  21712  recld2  21734  icccmplem2  21743  addcnlem  21783  divcn  21787  elcncf  21808  elcncf2  21809  cncfi  21813  rescncf  21816  mulc1cncf  21824  cncfco  21826  cncfmet  21827  cnheiborlem  21869  cnheibor  21870  cnllycmp  21871  evth  21874  htpycc  21895  phtpycc  21906  pcohtpylem  21934  pcoass  21939  pcorevlem  21941  nmoleub2lem2  22014  nmoleub3  22017  nmhmcn  22018  ipcau2  22092  ipcn  22101  lmmbr2  22113  lmmcvg  22115  lmmbrf  22116  fmcfil  22126  iscau2  22131  iscau4  22133  iscauf  22134  caucfil  22137  iscmet3lem3  22144  iscmet3lem1  22145  iscmet3lem2  22146  cfilresi  22149  cfilres  22150  caussi  22151  causs  22152  lmle  22155  lmclim  22156  bcthlem1  22176  bcthlem4  22179  bcth  22181  minveclem3b  22254  minveclem3  22255  minveclem4  22258  minveclem5  22259  minveclem7  22261  pmltpclem1  22271  pmltpc  22273  ivthlem1  22274  ivthlem2  22275  ivthlem3  22276  ivth  22277  cniccbdd  22284  ovolunlem1  22319  ovoliunlem1  22324  ovoliunlem2  22325  ovoliunlem3  22326  ovolshftlem1  22331  ovolscalem1  22335  ovolicc1  22338  ovolicc2lem3  22341  ovolicc2lem4  22342  ovolicc2lem5  22343  ioombl1lem4  22382  ioombl1  22383  uniioombllem6  22414  volsup2  22431  volcn  22432  mbfmulc2lem  22471  mbfsup  22488  mbflimsup  22491  mbflimsupOLD  22492  itg1climres  22540  mbfi1fseqlem6  22546  mbfi1fseq  22547  mbfi1flimlem  22548  itg2leub  22560  itg2seq  22568  itg2mulclem  22572  itg2monolem1  22576  itg2mono  22579  itg2i1fseq  22581  itg2addlem  22584  itg2gt0  22586  itg2cnlem1  22587  itg2cnlem2  22588  itg2cn  22589  bddmulibl  22664  itgcn  22668  ellimc3  22702  dveflem  22799  dvferm1lem  22804  dvferm2lem  22806  rolle  22810  dvlip  22813  dvlipcn  22814  dvlip2  22815  c1liplem1  22816  c1lip3  22819  dvge0  22826  dvivthlem1  22828  lhop1lem  22833  lhop1  22834  dvcvx  22840  dvfsumabs  22843  dvfsumlem2  22847  dvfsumrlim  22851  ftc1a  22857  ftc1lem4  22859  ftc1lem6  22861  itgsubstlem  22868  mdegleb  22881  mdegmullem  22895  deg1lt0  22908  ply1divmo  22952  ply1divex  22953  ply1divalg2  22955  q1peqb  22971  fta1g  22984  dgrub  23047  coe1termlem  23071  dgrcolem2  23087  dgrco  23088  quotval  23104  plydivlem3  23107  plydivlem4  23108  plydivex  23109  plydivalg  23111  quotlem  23112  plyrem  23117  fta1  23120  aannenlem1  23140  aannenlem2  23141  aalioulem3  23146  aalioulem4  23147  aalioulem5  23148  aalioulem6  23149  aaliou  23150  aaliou2  23152  aaliou2b  23153  ulmval  23191  ulm2  23196  ulmclm  23198  ulmshftlem  23200  ulmcaulem  23205  ulmcau  23206  ulmss  23208  ulmcn  23210  ulmdvlem1  23211  ulmdvlem3  23213  mtestbdd  23216  iblulm  23218  itgulm  23219  radcnvlem1  23224  pserulm  23233  abelthlem2  23243  abelthlem5  23246  abelthlem7  23249  abelthlem8  23250  abelthlem9  23251  abelth  23252  pilem3  23265  pilem3OLD  23266  sincosq2sgn  23310  sincosq3sgn  23311  sincosq4sgn  23312  logltb  23405  logcnlem5  23447  cxpcn3lem  23543  cxpcn3  23544  cxpaddle  23548  logreclem  23555  rlimcnp  23747  rlimcnp2  23748  xrlimcnp  23750  rlimcxp  23755  cxploglim  23759  jensen  23770  emcllem6  23782  emcllem7  23783  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem5  23814  lgamgulmlem6  23815  lgambdd  23818  lgamucov  23819  lgamcvglem  23821  ftalem2  23854  ftalem3  23855  ftalem5  23857  sqfpc  23918  mumullem2  23961  sqff1o  23963  chtublem  23993  chtub  23994  fsumvma2  23996  chpchtsum  24001  logexprlim  24007  bposlem6  24071  lgslem2  24079  lgslem3  24080  lgsval  24082  lgsfcl2  24084  lgsfle1  24087  lgsle1  24093  lgsdirprm  24111  chtppilimlem2  24166  chtppilim  24167  dchrisumlema  24180  dchrisumlem1  24181  dchrisumlem2  24182  dchrisumlem3  24183  dchrisum  24184  dchrmusumlema  24185  dchrvmasumlem2  24190  dchrisum0flblem1  24200  dchrisum0lema  24206  2vmadivsumlem  24232  chpdifbndlem1  24245  selberg3lem1  24249  selberg4lem1  24252  pntrsumbnd  24258  pntrsumbnd2  24259  selbergsb  24267  pntrlog2bndlem3  24271  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntpbnd1  24278  pntpbnd2  24279  pntibndlem2  24283  pntibndlem3  24284  pntibnd  24285  pntlemn  24292  pntlemj  24295  pntlemi  24296  pntlemo  24299  pntlem3  24301  pntlemp  24302  pntleml  24303  pnt3  24304  padicabv  24322  ostth2lem2  24326  ostth3  24330  ostth  24331  mirbtwnhl  24575  foot  24612  footeq  24614  mideulem2  24624  opphllem6  24642  hpgbr  24649  lmieu  24673  brbtwn2  24772  colinearalg  24777  axcontlem10  24840  umgrale  24885  umgrafi  24886  umgra1  24890  uslgra1  24936  1pthoncl  25158  2pthoncl  25169  clwlkisclwwlk2  25354  0eusgraiff0rgra  25503  umgrabi  25547  frgrawopreglem2  25609  isnvlem  26065  nvelbl  26161  nvelbl2  26162  nmoofval  26239  nmosetn0  26242  nmoolb  26248  nmoubi  26249  nmounbseqi  26254  nmounbseqiALT  26255  nmobndseqi  26256  nmobndseqiALT  26257  bloval  26258  isblo  26259  nmoo0  26268  nmlno0lem  26270  blocnilem  26281  siilem2  26329  ubthlem1  26348  ubthlem2  26349  ubthlem3  26350  ubth  26351  minvecolem3  26354  minvecolem4  26358  minvecolem5  26359  minvecolem7  26361  htthlem  26396  htth  26397  h2hcau  26458  h2hlm  26459  normlem7tALT  26598  norm3lemt  26631  hcau  26663  hlimi  26667  hlim2  26671  cmcm3  27094  pjnorm  27203  pjnel  27205  elcnop  27336  elbdop  27339  nmopsetn0  27344  nmfnsetn0  27357  elcnfn  27361  hhcno  27383  hhcnf  27384  nmoplb  27386  nmopub  27387  cnopc  27392  nmfnlb  27403  nmfnleub  27404  cnfnc  27409  idcnop  27460  nmop0  27465  nmfn0  27466  nmlnop0iALT  27474  nmcexi  27505  nmcopexi  27506  lnconi  27512  lnopcon  27514  nmcfnexi  27530  lnfncon  27535  branmfn  27584  leop3  27604  opsqrlem6  27624  cvmd  27815  cvdmd  27816  cvexch  27853  cdj3i  27920  fmptcof2  28090  xraddge02  28168  xdivpnfrp  28231  omndadd  28298  omndmul  28306  archirngz  28335  archiabllem2a  28340  isorng  28392  madjusmdetlem2  28484  locfinreflem  28497  locfinref  28498  sqsscirc2  28545  cnre2csqlem  28546  xrge0iifiso  28571  lmdvg  28589  qqhcn  28625  qqhucn  28626  esum2d  28744  brfae  28901  dya2ub  28922  omssubadd  28952  carsgmon  28966  oddpwdc  29004  eulerpartlemd  29016  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemimin  29155  ballotlemic  29156  ballotlemsv  29159  ballotlemfrcn0  29179  ballotlemrc  29180  sgnmul  29192  sgnmulsgn  29199  signsply0  29219  signswch  29229  signsvfn  29250  signsvfnn  29254  signlem0  29255  erdszelem8  29700  kur14  29718  snmlval  29833  snmlflim  29834  sinccvg  30096  abs2sqle  30103  abs2sqlt  30104  faclim2  30162  br1steqg  30194  br2ndeqg  30195  poseq  30269  soseq  30270  sltval  30312  brimg  30480  cgrtriv  30545  cgrdegen  30547  brofs  30548  cgrextend  30551  segconeu  30554  fvtransport  30575  transportprops  30577  brifs  30586  ifscgr  30587  brcgr3  30589  cgrxfr  30598  brfs  30622  btwnconn1lem7  30636  btwnconn1lem11  30640  btwnconn1lem12  30641  btwnconn1lem14  30643  brsegle  30651  segleantisym  30658  outsideofeu  30674  nn0prpwlem  30754  nn0prpw  30755  nndivlub  30894  poimirlem28  31662  poimirlem29  31663  poimirlem31  31665  poimir  31667  heicant  31669  dvtanlemOLD  31685  itg2addnclem  31687  itg2addnclem3  31689  itg2addnc  31690  itg2gt0cn  31691  bddiblnc  31706  ftc1cnnclem  31709  ftc1cnnc  31710  ftc1anclem5  31715  ftc1anclem6  31716  ftc1anc  31719  areacirclem1  31726  areacirclem2  31727  areacirclem4  31729  areacirclem5  31730  areacirc  31731  seqpo  31770  incsequz2  31772  lmclim2  31781  geomcau  31782  caushft  31784  prdsbnd  31819  ismtyima  31829  heiborlem4  31840  heiborlem6  31842  heiborlem7  31843  bfplem1  31848  bfplem2  31849  rrndstprj2  31857  rrncmslem  31858  rrnequiv  31861  oposlem  32447  opltcon2b  32471  pats  32550  ishlat1  32617  cvrexch  32684  atle  32700  athgt  32720  1cvrco  32736  3atlem5  32751  4atlem3  32860  dalawlem15  33149  lhprelat3N  33304  lautle  33348  lautcvr  33356  ltrnatb  33401  ltrneq2  33412  cdlemefr32sn2aw  33670  cdlemefs32sn1aw  33680  cdleme32fvaw  33705  cdleme35sn3a  33725  cdleme46frvlpq  33770  cdleme48gfv  33803  trlord  33835  cdlemg1fvawlemN  33839  cdlemg7fvbwN  33873  cdlemg31d  33966  istendo  34026  dva1dim  34251  dvhb1dimN  34252  diafval  34298  diaelval  34300  cdlemm10N  34385  dihopelvalcpre  34515  dihmeetcN  34569  dihmeetlem6  34576  dihjatc1  34578  irrapxlem3  35368  irrapxlem4  35369  irrapxlem5  35370  irrapxlem6  35371  pellexlem3  35375  monotoddzz  35487  jm2.19  35544  rmydioph  35565  fnwe2lem2  35605  hbtlem1  35678  hbtlem2  35679  hbtlem7  35680  hbtlem4  35681  hbtlem5  35683  hbtlem6  35684  dgrsub2  35690  fiuneneq  35760  rp-isfinite5  35851  frege124d  35982  frege92  36178  leeq1d  36222  extoimad  36234  isprm7  36287  nzss  36293  evth2f  36966  evthf  36978  cncmpmax  36983  rfcnpre4  36985  supxrgere  37155  suplesup  37161  fmul01  37220  climinf  37246  climinfOLD  37247  climsuse  37249  mullimc  37258  ellimcabssub0  37259  climf  37264  mullimcf  37265  idlimc  37268  limcperiod  37270  clim2f  37278  limsupre  37283  limsupreOLD  37284  limcleqr  37287  limclner  37294  clim0cf  37297  cncfshift  37313  cncfperiod  37318  fperdvper  37352  dvbdfbdioolem2  37363  dvbdfbdioo  37364  ioodvbdlimc1lem1  37365  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  stoweidlem7  37426  stoweidlem9  37428  stoweidlem15  37434  stoweidlem16  37435  stoweidlem18  37437  stoweidlem21  37440  stoweidlem26  37445  stoweidlem31  37451  stoweidlem34  37454  stoweidlem36  37456  stoweidlem37  37457  stoweidlem41  37461  stoweidlem44  37464  stoweidlem45  37465  stoweidlem46  37466  stoweidlem48  37468  stoweidlem51  37471  stoweidlem52  37472  stoweidlem55  37475  stoweidlem59  37479  stoweidlem60  37480  fourierdlem20  37548  fourierdlem25  37553  fourierdlem37  37565  fourierdlem39  37567  fourierdlem41  37569  fourierdlem48  37576  fourierdlem49  37577  fourierdlem50  37578  fourierdlem54  37582  fourierdlem64  37592  fourierdlem68  37596  fourierdlem70  37598  fourierdlem71  37599  fourierdlem73  37601  fourierdlem79  37607  fourierdlem80  37608  fourierdlem87  37615  fourierdlem96  37624  fourierdlem97  37625  fourierdlem98  37626  fourierdlem99  37627  fourierdlem103  37631  fourierdlem104  37632  fourierdlem105  37633  fourierdlem108  37636  fourierdlem109  37637  fourierdlem111  37639  fourierswlem  37652  fouriersw  37653  etransclem31  37687  etransclem47  37703  etransclem48  37704  etransc  37705  omessle  37818  iccpartlt  38118  iccpartltu  38119  iccpartgt  38121  iccpartleu  38122  iccpartrn  38124  iccpartiun  38128  icceuelpartlem  38129  iccpartdisj  38131  iccpartnel  38132  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  bgoldbtbnd  38284  pgrpgt2nabl  38901  ply1mulgsumlem1  38928  ply1mulgsumlem2  38929  divge1b  39058  divgt1b  39059  divlt1lt  39060  logge0b  39093  loggt0b  39094  regt1loggt0  39098  elbigo  39113  elbigolo1  39119  logblt1b  39126  nnlog2ge0lt1  39128  logbpw2m1  39129  blenpw2m1  39141
  Copyright terms: Public domain W3C validator