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

Theorem breq1d 4377
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 4370 . 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 1399   class class class wbr 4367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368
This theorem is referenced by:  eqbrtrd  4387  syl6eqbr  4404  sbcbr2g  4422  pofun  4730  dffv2  5847  fmptco  5966  isorel  6123  soisores  6124  soisoi  6125  isocnv  6127  isotr  6133  f1owe  6150  weniso  6151  caovordig  6379  caovordg  6381  caovord  6385  f1oweALT  6683  frxp  6809  xporderlem  6810  fnwelem  6814  reldmtpos  6881  brtpos  6882  tpostpos  6893  tposoprab  6909  ensn1g  7499  fndmeng  7511  xpsneng  7521  xpcomco  7526  pwdom  7588  snnen2o  7625  supgtoreq  7843  ordtypelem6  7863  ordtypelem7  7864  wdompwdom  7919  infdiffi  7988  r1sdom  8105  pm54.43  8294  prdom2  8297  indcardi  8335  alephordi  8368  cdalepw  8489  fin23lem26  8618  fin23lem23  8619  fin23lem22  8620  fin23lem27  8621  uniimadomf  8833  alephval2  8860  inar1  9064  nqereu  9218  ltrnq  9268  prlem934  9322  prlem936  9336  ltasr  9388  addgt0sr  9392  axpre-ltadd  9455  axpre-sup  9457  ltsubadd  9940  lesubadd  9942  ltaddsub2  9945  leaddsub2  9947  ltaddpos  9960  lesub2  9965  ltnegcon2  9972  lenegcon2  9975  addge01  9980  subge0  9983  suble0  9984  lesub0  9987  ltordlem  9995  mulgt1  10318  ltmulgt11  10319  gt0div  10325  ge0div  10326  ltmuldiv  10332  ltmuldiv2  10333  lemuldiv2  10341  ltrec  10342  lerec2  10349  ltdiv23  10352  lediv23  10353  addltmul  10691  avglt1  10693  avgle1  10695  avgle  10697  zlem1lt  10832  zgt0ge1  10834  rpnnen1lem5  11131  reexALT  11133  xrmin2  11300  xltnegi  11336  xmulval  11345  xlesubadd  11376  xmullem2  11378  nn0disj  11713  dfceil2  11868  uzenom  11978  seqf1olem1  12049  leexp2r  12126  sqlecan  12177  expmulnbnd  12200  hashbnd  12313  hashle00  12369  hashgt12el2  12386  hashf1  12410  seqcoll  12416  hashge3el3dif  12428  swrdccatin2  12623  swrd2lsw  12801  2swrd2eqwrdeq  12802  shftfval  12905  shftfib  12907  shftfn  12908  2shfti  12915  shftidt2  12916  sqrlem1  13078  sqrlem2  13079  sqrlem6  13083  sqrlem7  13084  absdiflt  13152  absdifle  13153  lenegsq  13155  cau3lem  13189  limsupgle  13302  limsupgre  13306  clim  13319  rlim  13320  rlim2  13321  clim2  13329  clim0  13331  clim0c  13332  rlim0  13333  rlim0lt  13334  climi0  13337  ello1  13340  ello1mpt  13346  elo1  13351  lo1o1  13357  rlimclim1  13370  rlimclim  13371  climrlim2  13372  rlimuni  13375  climuni  13377  lo1res  13384  rlimresb  13390  rlimeq  13394  2clim  13397  climshftlem  13399  climshft  13401  climabs0  13410  o1co  13411  rlimcn1  13413  rlimcn2  13415  climcn1  13416  climcn2  13417  addcn2  13418  subcn2  13419  mulcn2  13420  o1of2  13437  o1rlimmul  13443  rlimdiv  13470  rlimno1  13478  isershft  13488  isercoll  13492  climsup  13494  climcau  13495  caucvgrlem  13497  caucvgrlem2  13499  caurcvg2  13502  caucvg  13503  caucvgb  13504  serf0  13505  iseraltlem2  13507  iseralt  13509  sumeq1  13513  sumeq2w  13516  sumeq2ii  13517  sumrb  13537  summolem2  13540  summo  13541  zsum  13542  o1fsum  13629  cvgcmp  13632  cvgcmpce  13634  isumshft  13653  climcndslem1  13663  geolim  13681  geolim2  13682  geoisum1c  13691  mertenslem1  13695  mertenslem2  13696  mertens  13697  ntrivcvg  13708  ntrivcvgn0  13709  ntrivcvgmullem  13712  prodeq1f  13717  prodeq2w  13721  prodeq2ii  13722  prodrblem2  13740  prodmolem2  13744  prodmo  13745  zprod  13746  fprodntriv  13751  sin01bnd  13922  cos01bnd  13923  rpnnen  13962  ruclem9  13973  ruclem12  13976  sadcaddlem  14109  gcddvds  14155  dvdssq  14200  isprm  14221  isprm2lem  14226  prmgt1  14238  prmn2uzge3  14239  isprm6  14252  isprm5  14255  odzdvds  14324  pclem  14364  pcprecl  14365  pcprendvds  14366  pcpremul  14369  pcval  14370  pceulem  14371  pczndvds  14390  pcelnn  14395  pc2dvds  14404  pcadd  14410  pcadd2  14411  pcmpt  14413  prmpwdvds  14424  prmreclem1  14436  prmreclem5  14440  prmreclem6  14441  4sqlem17  14481  vdwlem10  14510  ramval  14528  0ram  14540  ram0  14542  ramz2  14544  ramub1lem2  14547  imasaddfnlem  14935  imasvscafn  14944  imasleval  14948  mreexexlemd  15051  symggen  16612  oddvdsnn0  16685  oddvds  16688  odf1  16701  odf1o1  16709  odf1o2  16710  gexdvds  16721  sylow1lem3  16737  efginvrel2  16862  efgsfo  16874  efgredlemd  16879  efgredlem  16882  efgred  16883  gexexlem  16975  torsubg  16977  oddvdssubg  16978  lt6abl  17014  ablfacrplem  17229  ablfacrp  17230  ablfaclem3  17251  abvfval  17580  abvpropd  17604  evlslem2  18293  znf1o  18681  znidomb  18691  cygznlem1  18696  frlmup1  18918  islinds  18929  lindsss  18944  chfacfscmul0  19444  chfacfscmulfsupp  19445  chfacfpmmul0  19448  chfacfpmmulfsupp  19449  cayleyhamilton1  19478  cctop  19592  ordthmeolem  20387  csdfil  20480  ufilen  20516  ptcmplem2  20638  ptcmplem3  20639  cnextfvval  20650  prdsxmetlem  20956  blfvalps  20971  elblps  20975  elbl  20976  elbl3ps  20979  elbl3  20980  blres  21019  imasf1obl  21076  blcld  21093  comet  21101  stdbdmetval  21102  stdbdbl  21105  metcnp2  21130  txmetcnp  21135  dscopn  21179  ngptgp  21235  nlmvscn  21281  nrginvrcn  21285  nmoval  21307  nghmcn  21337  cnbl0  21366  cnblcld  21367  bl2ioo  21382  recld2  21404  icccmplem2  21413  addcnlem  21453  divcn  21457  elcncf  21478  elcncf2  21479  cncfi  21483  rescncf  21486  mulc1cncf  21494  cncfco  21496  cncfmet  21497  cnheiborlem  21539  cnheibor  21540  cnllycmp  21541  evth  21544  htpycc  21565  phtpycc  21576  pcohtpylem  21604  pcoass  21609  pcorevlem  21611  nmoleub2lem2  21684  nmoleub3  21687  nmhmcn  21688  ipcau2  21762  ipcn  21771  lmmbr2  21783  lmmcvg  21785  lmmbrf  21786  fmcfil  21796  iscau2  21801  iscau4  21803  iscauf  21804  caucfil  21807  iscmet3lem3  21814  iscmet3lem1  21815  iscmet3lem2  21816  cfilresi  21819  cfilres  21820  caussi  21821  causs  21822  lmle  21825  lmclim  21826  bcthlem1  21848  bcthlem4  21851  bcth  21853  minveclem3b  21928  minveclem3  21929  minveclem4  21932  minveclem5  21933  minveclem7  21935  pmltpclem1  21945  pmltpc  21947  ivthlem1  21948  ivthlem2  21949  ivthlem3  21950  ivth  21951  cniccbdd  21958  ovolunlem1  21993  ovoliunlem1  21998  ovoliunlem2  21999  ovoliunlem3  22000  ovolshftlem1  22005  ovolscalem1  22009  ovolicc1  22012  ovolicc2lem3  22015  ovolicc2lem4  22016  ovolicc2lem5  22017  ioombl1lem4  22056  ioombl1  22057  uniioombllem6  22082  volsup2  22099  volcn  22100  mbfmulc2lem  22139  mbfsup  22156  mbflimsup  22158  itg1climres  22206  mbfi1fseqlem6  22212  mbfi1fseq  22213  mbfi1flimlem  22214  itg2leub  22226  itg2seq  22234  itg2mulclem  22238  itg2monolem1  22242  itg2mono  22245  itg2i1fseq  22247  itg2addlem  22250  itg2gt0  22252  itg2cnlem1  22253  itg2cnlem2  22254  itg2cn  22255  bddmulibl  22330  itgcn  22334  ellimc3  22368  dveflem  22465  dvferm1lem  22470  dvferm2lem  22472  rolle  22476  dvlip  22479  dvlipcn  22480  dvlip2  22481  c1liplem1  22482  c1lip3  22485  dvge0  22492  dvivthlem1  22494  lhop1lem  22499  lhop1  22500  dvcvx  22506  dvfsumabs  22509  dvfsumlem2  22513  dvfsumrlim  22517  ftc1a  22523  ftc1lem4  22525  ftc1lem6  22527  itgsubstlem  22534  mdegleb  22549  mdegmullem  22563  deg1lt0  22576  ply1divmo  22621  ply1divex  22622  ply1divalg2  22624  q1peqb  22640  fta1g  22653  dgrub  22716  coe1termlem  22740  dgrcolem2  22756  dgrco  22757  quotval  22773  plydivlem3  22776  plydivlem4  22777  plydivex  22778  plydivalg  22780  quotlem  22781  plyrem  22786  fta1  22789  aannenlem1  22809  aannenlem2  22810  aalioulem3  22815  aalioulem4  22816  aalioulem5  22817  aalioulem6  22818  aaliou  22819  aaliou2  22821  aaliou2b  22822  ulmval  22860  ulm2  22865  ulmclm  22867  ulmshftlem  22869  ulmcaulem  22874  ulmcau  22875  ulmss  22877  ulmcn  22879  ulmdvlem1  22880  ulmdvlem3  22882  mtestbdd  22885  iblulm  22887  itgulm  22888  radcnvlem1  22893  pserulm  22902  abelthlem2  22912  abelthlem5  22915  abelthlem7  22918  abelthlem8  22919  abelthlem9  22920  abelth  22921  pilem3  22933  sincosq2sgn  22977  sincosq3sgn  22978  sincosq4sgn  22979  logltb  23072  logcnlem5  23114  cxpcn3lem  23208  cxpcn3  23209  cxpaddle  23213  logreclem  23220  rlimcnp  23412  rlimcnp2  23413  xrlimcnp  23415  rlimcxp  23420  cxploglim  23424  jensen  23435  emcllem6  23447  emcllem7  23448  ftalem2  23464  ftalem3  23465  ftalem5  23467  sqfpc  23528  mumullem2  23571  sqff1o  23573  chtublem  23603  chtub  23604  fsumvma2  23606  chpchtsum  23611  logexprlim  23617  bposlem6  23681  lgslem2  23689  lgslem3  23690  lgsval  23692  lgsfcl2  23694  lgsfle1  23697  lgsle1  23703  lgsdirprm  23721  chtppilimlem2  23776  chtppilim  23777  dchrisumlema  23790  dchrisumlem1  23791  dchrisumlem2  23792  dchrisumlem3  23793  dchrisum  23794  dchrmusumlema  23795  dchrvmasumlem2  23800  dchrisum0flblem1  23810  dchrisum0lema  23816  2vmadivsumlem  23842  chpdifbndlem1  23855  selberg3lem1  23859  selberg4lem1  23862  pntrsumbnd  23868  pntrsumbnd2  23869  selbergsb  23877  pntrlog2bndlem3  23881  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  pntpbnd1  23888  pntpbnd2  23889  pntibndlem2  23893  pntibndlem3  23894  pntibnd  23895  pntlemn  23902  pntlemj  23905  pntlemi  23906  pntlemo  23909  pntlem3  23911  pntlemp  23912  pntleml  23913  pnt3  23914  padicabv  23932  ostth2lem2  23936  ostth3  23940  ostth  23941  mirbtwnhl  24180  foot  24216  footeq  24218  mideulem2  24228  opphllem6  24244  hpgbr  24249  lmieu  24270  iscgra  24289  cgraid  24290  brbtwn2  24329  colinearalg  24334  axcontlem10  24397  umgrale  24442  umgrafi  24443  umgra1  24447  uslgra1  24493  1pthoncl  24715  2pthoncl  24726  clwlkisclwwlk2  24911  0eusgraiff0rgra  25060  umgrabi  25104  frgrawopreglem2  25166  isnvlem  25620  nvelbl  25716  nvelbl2  25717  nmoofval  25794  nmosetn0  25797  nmoolb  25803  nmoubi  25804  nmounbseqi  25809  nmounbseqiALT  25810  nmobndseqi  25811  nmobndseqiALT  25812  bloval  25813  isblo  25814  nmoo0  25823  nmlno0lem  25825  blocnilem  25836  siilem2  25884  ubthlem1  25903  ubthlem2  25904  ubthlem3  25905  ubth  25906  minvecolem3  25909  minvecolem4  25913  minvecolem5  25914  minvecolem7  25916  htthlem  25951  htth  25952  h2hcau  26013  h2hlm  26014  normlem7tALT  26153  norm3lemt  26186  hcau  26218  hlimi  26222  hlim2  26226  cmcm3  26650  pjnorm  26759  pjnel  26761  elcnop  26892  elbdop  26895  nmopsetn0  26900  nmfnsetn0  26913  elcnfn  26917  hhcno  26939  hhcnf  26940  nmoplb  26942  nmopub  26943  cnopc  26948  nmfnlb  26959  nmfnleub  26960  cnfnc  26965  idcnop  27016  nmop0  27021  nmfn0  27022  nmlnop0iALT  27030  nmcexi  27061  nmcopexi  27062  lnconi  27068  lnopcon  27070  nmcfnexi  27086  lnfncon  27091  branmfn  27140  leop3  27160  opsqrlem6  27180  cvmd  27371  cvdmd  27372  cvexch  27409  cdj3i  27476  fmptcof2  27643  xraddge02  27727  xdivpnfrp  27782  omndadd  27849  omndmul  27857  archirngz  27886  archiabllem2a  27891  isorng  27943  locfinreflem  27997  locfinref  27998  sqsscirc2  28045  cnre2csqlem  28046  xrge0iifiso  28071  lmdvg  28089  qqhcn  28125  qqhucn  28126  esum2d  28241  brfae  28376  dya2ub  28397  omssubadd  28427  carsgmon  28441  oddpwdc  28476  eulerpartlemd  28488  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemimin  28627  ballotlemic  28628  ballotlemsv  28631  ballotlemfrcn0  28651  ballotlemrc  28652  sgnmul  28664  sgnmulsgn  28671  signsply0  28691  signswch  28701  signsvfn  28722  signsvfnn  28726  signlem0  28727  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem5  28764  lgamgulmlem6  28765  lgambdd  28768  lgamucov  28769  lgamcvglem  28771  erdszelem8  28831  kur14  28849  snmlval  28965  snmlflim  28966  sinccvg  29228  abs2sqle  29235  abs2sqlt  29236  faclim2  29339  poseq  29498  soseq  29499  sltval  29572  brimg  29740  cgrtriv  29805  cgrdegen  29807  brofs  29808  cgrextend  29811  segconeu  29814  fvtransport  29835  transportprops  29837  brifs  29846  ifscgr  29847  brcgr3  29849  cgrxfr  29858  brfs  29882  btwnconn1lem7  29896  btwnconn1lem11  29900  btwnconn1lem12  29901  btwnconn1lem14  29903  brsegle  29911  segleantisym  29918  outsideofeu  29934  nndivlub  30076  heicant  30214  dvtanlemOLD  30230  itg2addnclem  30232  itg2addnclem3  30234  itg2addnc  30235  itg2gt0cn  30236  bddiblnc  30251  ftc1cnnclem  30254  ftc1cnnc  30255  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anc  30264  areacirclem1  30273  areacirclem2  30274  areacirclem4  30276  areacirclem5  30277  areacirc  30278  nn0prpwlem  30306  nn0prpw  30307  seqpo  30406  incsequz2  30408  lmclim2  30417  geomcau  30418  caushft  30420  prdsbnd  30455  ismtyima  30465  heiborlem4  30476  heiborlem6  30478  heiborlem7  30479  bfplem1  30484  bfplem2  30485  rrndstprj2  30493  rrncmslem  30494  rrnequiv  30497  irrapxlem3  30925  irrapxlem4  30926  irrapxlem5  30927  irrapxlem6  30928  pellexlem3  30932  monotoddzz  31044  jm2.19  31101  rmydioph  31122  fnwe2lem2  31163  hbtlem1  31240  hbtlem2  31241  hbtlem7  31242  hbtlem4  31243  hbtlem5  31245  hbtlem6  31246  dgrsub2  31252  fiuneneq  31322  isprm7  31360  lcmgcdlem  31380  lcmdvds  31382  nzss  31390  evth2f  31557  evthf  31569  cncmpmax  31574  rfcnpre4  31576  fmul01  31740  climinf  31778  climsuse  31780  mullimc  31788  ellimcabssub0  31789  climf  31794  mullimcf  31795  idlimc  31798  limcperiod  31800  clim2f  31808  limsupre  31813  limcleqr  31816  limclner  31823  clim0cf  31826  cncfshift  31842  cncfperiod  31847  fperdvper  31881  dvbdfbdioolem2  31892  dvbdfbdioo  31893  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  stoweidlem7  31955  stoweidlem9  31957  stoweidlem15  31963  stoweidlem16  31964  stoweidlem18  31966  stoweidlem21  31969  stoweidlem26  31974  stoweidlem31  31979  stoweidlem34  31982  stoweidlem36  31984  stoweidlem37  31985  stoweidlem41  31989  stoweidlem44  31992  stoweidlem45  31993  stoweidlem46  31994  stoweidlem48  31996  stoweidlem51  31999  stoweidlem52  32000  stoweidlem55  32003  stoweidlem59  32007  stoweidlem60  32008  fourierdlem20  32075  fourierdlem25  32080  fourierdlem37  32092  fourierdlem39  32094  fourierdlem41  32096  fourierdlem48  32103  fourierdlem49  32104  fourierdlem50  32105  fourierdlem54  32109  fourierdlem64  32119  fourierdlem68  32123  fourierdlem70  32125  fourierdlem71  32126  fourierdlem73  32128  fourierdlem79  32134  fourierdlem80  32135  fourierdlem87  32142  fourierdlem96  32151  fourierdlem97  32152  fourierdlem98  32153  fourierdlem99  32154  fourierdlem103  32158  fourierdlem104  32159  fourierdlem105  32160  fourierdlem108  32163  fourierdlem109  32164  fourierdlem111  32166  fourierswlem  32179  fouriersw  32180  etransclem31  32214  etransclem47  32230  etransclem48  32231  etransc  32232  pgrpgt2nabl  33159  ply1mulgsumlem1  33186  ply1mulgsumlem2  33187  divge1b  33316  divgt1b  33317  divlt1lt  33318  logge0b  33352  loggt0b  33353  regt1loggt0  33357  elbigo  33372  elbigolo1  33378  logblt1b  33385  nnlog2ge0lt1  33387  logbpw2m1  33388  blenpw2m1  33400  oposlem  35320  opltcon2b  35344  pats  35423  ishlat1  35490  cvrexch  35557  atle  35573  athgt  35593  1cvrco  35609  3atlem5  35624  4atlem3  35733  dalawlem15  36022  lhprelat3N  36177  lautle  36221  lautcvr  36229  ltrnatb  36274  ltrneq2  36285  cdlemefr32sn2aw  36543  cdlemefs32sn1aw  36553  cdleme32fvaw  36578  cdleme35sn3a  36598  cdleme46frvlpq  36643  cdleme48gfv  36676  trlord  36708  cdlemg1fvawlemN  36712  cdlemg7fvbwN  36746  cdlemg31d  36839  istendo  36899  dva1dim  37124  dvhb1dimN  37125  diafval  37171  diaelval  37173  cdlemm10N  37258  dihopelvalcpre  37388  dihmeetcN  37442  dihmeetlem6  37449  dihjatc1  37451  rp-isfinite5  38172  frege92  38454  leeq1d  38498  extoimad  38510
  Copyright terms: Public domain W3C validator