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

Theorem breq1d 4400
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 4393 . 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 1370   class class class wbr 4390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391
This theorem is referenced by:  eqbrtrd  4410  syl6eqbr  4427  sbcbr2g  4446  pofun  4755  dffv2  5863  fmptco  5975  isorel  6116  soisores  6117  soisoi  6118  isocnv  6120  isotr  6126  f1owe  6143  weniso  6144  caovordig  6368  caovordg  6370  caovord  6374  f1oweALT  6661  frxp  6782  xporderlem  6783  fnwelem  6787  reldmtpos  6853  brtpos  6854  tpostpos  6865  tposoprab  6881  th3qlem2  7307  ensn1g  7474  fndmeng  7486  xpsneng  7496  xpcomco  7501  pwdom  7563  snnen2o  7600  ordtypelem6  7838  ordtypelem7  7839  wdompwdom  7894  infdiffi  7964  r1sdom  8082  pm54.43  8271  prdom2  8274  indcardi  8312  alephordi  8345  cdalepw  8466  fin23lem26  8595  fin23lem23  8596  fin23lem22  8597  fin23lem27  8598  uniimadomf  8810  alephval2  8837  inar1  9043  nqereu  9199  ltrnq  9249  prlem934  9303  prlem936  9317  ltasr  9368  addgt0sr  9372  axpre-ltadd  9435  axpre-sup  9437  ltsubadd  9910  lesubadd  9912  ltaddsub2  9915  leaddsub2  9917  ltaddpos  9930  lesub2  9935  ltnegcon2  9942  lenegcon2  9945  addge01  9950  subge0  9953  suble0  9954  lesub0  9957  ltordlem  9966  mulgt1  10289  ltmulgt11  10290  gt0div  10296  ge0div  10297  ltmuldiv  10303  ltmuldiv2  10304  lemuldiv2  10313  ltrec  10314  lerec2  10321  ltdiv23  10324  lediv23  10325  addltmul  10661  avglt1  10663  avgle1  10665  avgle  10667  zlem1lt  10797  zgt0ge1  10799  rpnnen1lem5  11084  reexALT  11086  xrmin2  11251  xltnegi  11287  xmulval  11296  xlesubadd  11327  xmullem2  11329  dfceil2  11781  uzenom  11888  seqf1olem1  11946  leexp2r  12022  sqlecan  12073  expmulnbnd  12097  hashbnd  12210  hashle00  12260  hashgt12el2  12276  hashge3el3dif  12289  hashf1  12312  seqcoll  12318  lswccatn0lsw  12389  swrdccatin2  12480  swrd2lsw  12654  2swrd2eqwrdeq  12655  shftfval  12661  shftfib  12663  shftfn  12664  2shfti  12671  shftidt2  12672  sqrlem1  12834  sqrlem2  12835  sqrlem6  12839  sqrlem7  12840  absdiflt  12907  absdifle  12908  lenegsq  12910  cau3lem  12944  limsupgle  13057  limsupgre  13061  clim  13074  rlim  13075  rlim2  13076  clim2  13084  clim0  13086  clim0c  13087  rlim0  13088  rlim0lt  13089  climi0  13092  ello1  13095  ello1mpt  13101  elo1  13106  lo1o1  13112  rlimclim1  13125  rlimclim  13126  climrlim2  13127  rlimuni  13130  climuni  13132  lo1res  13139  rlimresb  13145  rlimeq  13149  2clim  13152  climshftlem  13154  climshft  13156  climabs0  13165  o1co  13166  rlimcn1  13168  rlimcn2  13170  climcn1  13171  climcn2  13172  addcn2  13173  subcn2  13174  mulcn2  13175  o1of2  13192  o1rlimmul  13198  rlimdiv  13225  rlimno1  13233  isershft  13243  isercoll  13247  climsup  13249  climcau  13250  caucvgrlem  13252  caucvgrlem2  13254  caurcvg2  13257  caucvg  13258  caucvgb  13259  serf0  13260  iseraltlem2  13262  iseralt  13264  sumeq1  13268  sumeq2w  13271  sumeq2ii  13272  sumrb  13292  summolem2  13295  summo  13296  zsum  13297  o1fsum  13378  cvgcmp  13381  cvgcmpce  13383  isumshft  13404  climcndslem1  13414  geolim  13432  geolim2  13433  geoisum1c  13442  mertenslem1  13446  mertenslem2  13447  mertens  13448  sin01bnd  13571  cos01bnd  13572  rpnnen  13611  ruclem9  13622  ruclem12  13625  sadcaddlem  13755  gcddvds  13801  dvdssq  13846  isprm  13867  isprm2lem  13872  prmgt1  13884  isprm6  13897  isprm5  13900  odzdvds  13969  pclem  14007  pcprecl  14008  pcprendvds  14009  pcpremul  14012  pcval  14013  pceulem  14014  pczndvds  14033  pcelnn  14038  pc2dvds  14047  pcadd  14053  pcadd2  14054  pcmpt  14056  prmpwdvds  14067  prmreclem1  14079  prmreclem5  14083  prmreclem6  14084  4sqlem17  14124  vdwlem10  14153  ramval  14171  0ram  14183  ram0  14185  ramz2  14187  ramub1lem2  14190  imasaddfnlem  14568  imasvscafn  14577  imasleval  14581  mreexexlemd  14684  symggen  16078  oddvdsnn0  16151  oddvds  16154  odf1  16167  odf1o1  16175  odf1o2  16176  gexdvds  16187  sylow1lem3  16203  efginvrel2  16328  efgsfo  16340  efgredlemd  16345  efgredlem  16348  efgred  16349  gexexlem  16438  torsubg  16440  oddvdssubg  16441  lt6abl  16475  ablfacrplem  16671  ablfacrp  16672  ablfaclem3  16693  abvfval  17009  abvpropd  17033  mptscmfsuppd  17118  evlslem2  17704  znf1o  18093  znidomb  18103  cygznlem1  18108  frlmup1  18335  islinds  18347  lindsss  18362  cctop  18726  ordthmeolem  19490  csdfil  19583  ufilen  19619  ptcmplem2  19741  ptcmplem3  19742  cnextfvval  19753  prdsxmetlem  20059  blfvalps  20074  elblps  20078  elbl  20079  elbl3ps  20082  elbl3  20083  blres  20122  imasf1obl  20179  blcld  20196  comet  20204  stdbdmetval  20205  stdbdbl  20208  metcnp2  20233  txmetcnp  20238  dscopn  20282  ngptgp  20338  nlmvscn  20384  nrginvrcn  20388  nmoval  20410  nghmcn  20440  cnbl0  20469  cnblcld  20470  bl2ioo  20485  recld2  20507  icccmplem2  20516  addcnlem  20556  divcn  20560  elcncf  20581  elcncf2  20582  cncfi  20586  rescncf  20589  mulc1cncf  20597  cncfco  20599  cncfmet  20600  cnheiborlem  20642  cnheibor  20643  cnllycmp  20644  evth  20647  htpycc  20668  phtpycc  20679  pcohtpylem  20707  pcoass  20712  pcorevlem  20714  nmoleub2lem2  20787  nmoleub3  20790  nmhmcn  20791  ipcau2  20865  ipcn  20874  lmmbr2  20886  lmmcvg  20888  lmmbrf  20889  fmcfil  20899  iscau2  20904  iscau4  20906  iscauf  20907  caucfil  20910  iscmet3lem3  20917  iscmet3lem1  20918  iscmet3lem2  20919  cfilresi  20922  cfilres  20923  caussi  20924  causs  20925  lmle  20928  lmclim  20929  bcthlem1  20951  bcthlem4  20954  bcth  20956  minveclem3b  21031  minveclem3  21032  minveclem4  21035  minveclem5  21036  minveclem7  21038  pmltpclem1  21048  pmltpc  21050  ivthlem1  21051  ivthlem2  21052  ivthlem3  21053  ivth  21054  cniccbdd  21061  ovolunlem1  21096  ovoliunlem1  21101  ovoliunlem2  21102  ovoliunlem3  21103  ovolshftlem1  21108  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem3  21118  ovolicc2lem4  21119  ovolicc2lem5  21120  ioombl1lem4  21158  ioombl1  21159  uniioombllem6  21184  volsup2  21201  volcn  21202  mbfmulc2lem  21241  mbfsup  21258  mbflimsup  21260  itg1climres  21308  mbfi1fseqlem6  21314  mbfi1fseq  21315  mbfi1flimlem  21316  itg2leub  21328  itg2seq  21336  itg2mulclem  21340  itg2monolem1  21344  itg2mono  21347  itg2i1fseq  21349  itg2addlem  21352  itg2gt0  21354  itg2cnlem1  21355  itg2cnlem2  21356  itg2cn  21357  bddmulibl  21432  itgcn  21436  ellimc3  21470  dveflem  21567  dvferm1lem  21572  dvferm2lem  21574  rolle  21578  dvlip  21581  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  c1lip3  21587  dvge0  21594  dvivthlem1  21596  lhop1lem  21601  lhop1  21602  dvcvx  21608  dvfsumabs  21611  dvfsumlem2  21615  dvfsumrlim  21619  ftc1a  21625  ftc1lem4  21627  ftc1lem6  21629  itgsubstlem  21636  mdegleb  21651  mdegmullem  21665  deg1lt0  21678  ply1divmo  21723  ply1divex  21724  ply1divalg2  21726  q1peqb  21742  fta1g  21755  dgrub  21818  coe1termlem  21841  dgrcolem2  21857  dgrco  21858  quotval  21874  plydivlem3  21877  plydivlem4  21878  plydivex  21879  plydivalg  21881  quotlem  21882  plyrem  21887  fta1  21890  aannenlem1  21910  aannenlem2  21911  aalioulem3  21916  aalioulem4  21917  aalioulem5  21918  aalioulem6  21919  aaliou  21920  aaliou2  21922  aaliou2b  21923  ulmval  21961  ulm2  21966  ulmclm  21968  ulmshftlem  21970  ulmcaulem  21975  ulmcau  21976  ulmss  21978  ulmcn  21980  ulmdvlem1  21981  ulmdvlem3  21983  mtestbdd  21986  iblulm  21988  itgulm  21989  radcnvlem1  21994  pserulm  22003  abelthlem2  22013  abelthlem5  22016  abelthlem7  22019  abelthlem8  22020  abelthlem9  22021  abelth  22022  pilem3  22034  sincosq2sgn  22077  sincosq3sgn  22078  sincosq4sgn  22079  logltb  22164  logcnlem5  22207  cxpcn3lem  22301  cxpcn3  22302  cxpaddle  22306  logreclem  22330  rlimcnp  22475  rlimcnp2  22476  xrlimcnp  22478  rlimcxp  22483  cxploglim  22487  jensen  22498  emcllem6  22510  emcllem7  22511  ftalem2  22527  ftalem3  22528  ftalem5  22530  sqfpc  22591  mumullem2  22634  sqff1o  22636  chtublem  22666  chtub  22667  fsumvma2  22669  chpchtsum  22674  logexprlim  22680  bposlem6  22744  lgslem2  22752  lgslem3  22753  lgsval  22755  lgsfcl2  22757  lgsfle1  22760  lgsle1  22766  lgsdirprm  22784  chtppilimlem2  22839  chtppilim  22840  dchrisumlema  22853  dchrisumlem1  22854  dchrisumlem2  22855  dchrisumlem3  22856  dchrisum  22857  dchrmusumlema  22858  dchrvmasumlem2  22863  dchrisum0flblem1  22873  dchrisum0lema  22879  2vmadivsumlem  22905  chpdifbndlem1  22918  selberg3lem1  22922  selberg4lem1  22925  pntrsumbnd  22931  pntrsumbnd2  22932  selbergsb  22940  pntrlog2bndlem3  22944  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntibndlem3  22957  pntibnd  22958  pntlemn  22965  pntlemj  22968  pntlemi  22969  pntlemo  22972  pntlem3  22974  pntlemp  22975  pntleml  22976  pnt3  22977  padicabv  22995  ostth2lem2  22999  ostth3  23003  ostth  23004  nehash2  23079  foot  23238  mideulem  23244  brbtwn2  23286  colinearalg  23291  axcontlem10  23354  umgrale  23390  umgrafi  23391  umgra1  23395  uslgra1  23426  1pthoncl  23626  2pthoncl  23637  umgrabi  23739  isnvlem  24123  nvelbl  24219  nvelbl2  24220  nmoofval  24297  nmosetn0  24300  nmoolb  24306  nmoubi  24307  nmounbseqi  24312  nmounbseqiOLD  24313  nmobndseqi  24314  nmobndseqiOLD  24315  bloval  24316  isblo  24317  nmoo0  24326  nmlno0lem  24328  blocnilem  24339  siilem2  24387  ubthlem1  24406  ubthlem2  24407  ubthlem3  24408  ubth  24409  minvecolem3  24412  minvecolem4  24416  minvecolem5  24417  minvecolem7  24419  htthlem  24454  htth  24455  h2hcau  24516  h2hlm  24517  normlem7tALT  24656  norm3lemt  24689  hcau  24721  hlimi  24725  hlim2  24729  cmcm3  25153  pjnorm  25262  pjnel  25264  elcnop  25396  elbdop  25399  nmopsetn0  25404  nmfnsetn0  25417  elcnfn  25421  hhcno  25443  hhcnf  25444  nmoplb  25446  nmopub  25447  cnopc  25452  nmfnlb  25463  nmfnleub  25464  cnfnc  25469  idcnop  25520  nmop0  25525  nmfn0  25526  nmlnop0iALT  25534  nmcexi  25565  nmcopexi  25566  lnconi  25572  lnopcon  25574  nmcfnexi  25590  lnfncon  25595  branmfn  25644  leop3  25664  opsqrlem6  25684  cvmd  25875  cvdmd  25876  cvexch  25913  cdj3i  25980  fmptcof2  26113  xraddge02  26184  xdivpnfrp  26242  omndadd  26303  omndmul  26311  archirngz  26340  archiabllem2a  26345  isorng  26401  sqsscirc2  26473  cnre2csqlem  26474  xrge0iifiso  26499  lmdvg  26517  qqhcn  26554  qqhucn  26555  brfae  26798  dya2ub  26819  oddpwdc  26871  eulerpartlemd  26883  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemimin  27022  ballotlemic  27023  ballotlemsv  27026  ballotlemfrcn0  27046  ballotlemrc  27047  sgnmul  27059  sgnmulsgn  27066  signsplypnf  27085  signsply0  27086  signswch  27096  signsvfn  27117  signsvfnn  27121  signlem0  27122  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgamgulmlem6  27154  lgambdd  27157  lgamucov  27158  lgamcvglem  27160  erdszelem8  27220  kur14  27238  snmlval  27354  snmlflim  27355  sinccvg  27452  abs2sqle  27459  abs2sqlt  27460  ntrivcvg  27546  ntrivcvgn0  27547  ntrivcvgmullem  27550  prodeq1f  27555  prodeq2w  27559  prodeq2ii  27560  prodrblem2  27578  prodmolem2  27582  prodmo  27583  zprod  27584  fprodntriv  27589  faclim2  27688  poseq  27848  soseq  27849  sltval  27922  brimg  28102  cgrtriv  28167  cgrdegen  28169  brofs  28170  cgrextend  28173  segconeu  28176  fvtransport  28197  transportprops  28199  brifs  28208  ifscgr  28209  brcgr3  28211  cgrxfr  28220  brfs  28244  btwnconn1lem7  28258  btwnconn1lem11  28262  btwnconn1lem12  28263  btwnconn1lem14  28265  brsegle  28273  segleantisym  28280  outsideofeu  28296  nndivlub  28438  heicant  28564  dvtanlem  28579  itg2addnclem  28581  itg2addnclem3  28583  itg2addnc  28584  itg2gt0cn  28585  bddiblnc  28600  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anc  28613  areacirclem1  28622  areacirclem2  28623  areacirclem4  28625  areacirclem5  28626  areacirc  28627  nn0prpwlem  28655  nn0prpw  28656  seqpo  28781  incsequz2  28783  lmclim2  28792  geomcau  28793  caushft  28795  prdsbnd  28830  ismtyima  28840  heiborlem4  28851  heiborlem6  28853  heiborlem7  28854  bfplem1  28859  bfplem2  28860  rrndstprj2  28868  rrncmslem  28869  rrnequiv  28872  irrapxlem3  29303  irrapxlem4  29304  irrapxlem5  29305  irrapxlem6  29306  pellexlem3  29310  monotoddzz  29422  jm2.19  29480  rmydioph  29501  fnwe2lem2  29542  hbtlem1  29617  hbtlem2  29618  hbtlem7  29619  hbtlem4  29620  hbtlem5  29622  hbtlem6  29623  dgrsub2  29629  fiuneneq  29700  evth2f  29875  evthf  29887  cncmpmax  29892  rfcnpre4  29894  fmul01  29899  climinf  29917  climsuse  29919  stoweidlem7  29940  stoweidlem9  29942  stoweidlem15  29948  stoweidlem16  29949  stoweidlem18  29951  stoweidlem21  29954  stoweidlem26  29959  stoweidlem31  29964  stoweidlem34  29967  stoweidlem36  29969  stoweidlem37  29970  stoweidlem41  29974  stoweidlem44  29977  stoweidlem45  29978  stoweidlem46  29979  stoweidlem48  29981  stoweidlem51  29984  stoweidlem52  29985  stoweidlem55  29988  stoweidlem59  29992  stoweidlem60  29993  prmn2uzge3  30387  clwlkisclwwlk2  30590  0eusgraiff0rgra  30690  frgrawopreglem2  30776  nn0disj  30876  supgtoreq  30881  pgrpgt2nabel  30909  ply1mulgsumlem1  30986  ply1mulgsumlem2  30987  chfacfscmul0  31312  chfacfscmulfsupp  31313  chfacfpmmul0  31316  chfacfpmmulfsupp  31317  cayleyhamilton1  31347  oposlem  33133  opltcon2b  33157  pats  33236  ishlat1  33303  cvrexch  33370  atle  33386  athgt  33406  1cvrco  33422  3atlem5  33437  4atlem3  33546  dalawlem15  33835  lhprelat3N  33990  lautle  34034  lautcvr  34042  ltrnatb  34087  ltrneq2  34098  cdlemefr32sn2aw  34354  cdlemefs32sn1aw  34364  cdleme32fvaw  34389  cdleme35sn3a  34409  cdleme46frvlpq  34454  cdleme48gfv  34487  trlord  34519  cdlemg1fvawlemN  34523  cdlemg7fvbwN  34557  cdlemg31d  34650  istendo  34710  dva1dim  34935  dvhb1dimN  34936  diafval  34982  diaelval  34984  cdlemm10N  35069  dihopelvalcpre  35199  dihmeetcN  35253  dihmeetlem6  35260  dihjatc1  35262
  Copyright terms: Public domain W3C validator