MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqd Structured version   Visualization version   GIF version

Theorem breqd 5073
Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
Hypothesis
Ref Expression
breq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
breqd (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))

Proof of Theorem breqd
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq 5064 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530   class class class wbr 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2817  df-clel 2897  df-br 5063
This theorem is referenced by:  breq123d  5076  breqdi  5077  sbcbr123  5116  sbcbr  5117  sbcbr12g  5118  fvmptopab  7204  brfvopab  7206  mptmpoopabbrd  7772  mptmpoopabovd  7773  bropopvvv  7779  bropfvvvvlem  7780  sprmpod  7884  wfrlem5  7953  supeq123d  8906  fpwwe2lem12  10055  fpwwe2  10057  brtrclfv  14355  dfrtrclrec2  14409  rtrclreclem3  14412  relexpindlem  14415  shftfib  14424  2shfti  14432  prdsval  16720  pwsle  16757  pwsleval  16758  imasleval  16806  issect  17015  isinv  17022  brcic  17060  ciclcl  17064  cicrcl  17065  isfunc  17126  funcres2c  17163  isfull  17172  isfth  17176  fullpropd  17182  fthpropd  17183  elhoma  17284  isposd  17557  pltval  17562  lubfval  17580  glbfval  17593  joinfval  17603  meetfval  17617  odumeet  17742  odujoin  17744  ipole  17760  eqgval  18261  unitpropd  19369  ltbval  20172  opsrval  20175  znleval  20617  lmbr  21782  metustexhalf  23081  metucn  23096  isphtpc  23513  taylthlem1  24876  ulmval  24883  tgjustf  26173  iscgrg  26212  legov  26285  ishlg  26302  opphllem5  26451  opphllem6  26452  hpgbr  26460  iscgra  26509  acopy  26534  isinag  26539  isleag  26548  iseqlg  26568  wlkonprop  27355  wksonproplem  27401  istrlson  27403  upgrwlkdvspth  27435  ispthson  27438  isspthson  27439  cyclispthon  27497  wspthsn  27541  wspthsnon  27545  iswspthsnon  27549  1pthon2v  27847  3wlkond  27865  dfconngr1  27882  isconngr  27883  isconngr1  27884  1conngr  27888  conngrv2edg  27889  minvecolem4b  28570  minvecolem4  28572  br8d  30277  ressprs  30557  resstos  30562  isomnd  30617  submomnd  30626  ogrpaddltrd  30635  isinftm  30725  isorng  30787  metidv  31019  pstmfval  31023  faeval  31392  brfae  31394  isacycgr  32277  isacycgr1  32278  issconn  32358  satfbrsuc  32498  mclsax  32701  fprlem1  33022  frrlem15  33027  bj-imdirval3  34354  unceq  34737  alrmomodm  35482  relbrcoss  35554  lcvbr  36025  isopos  36184  cmtvalN  36215  isoml  36242  cvrfval  36272  cvrval  36273  pats  36289  isatl  36303  iscvlat  36327  ishlat1  36356  llnset  36509  lplnset  36533  lvolset  36576  lineset  36742  psubspset  36748  pmapfval  36760  lautset  37086  ldilfset  37112  ltrnfset  37121  trlfset  37164  diaffval  38034  dicffval  38178  dihffval  38234  fnwe2lem2  39513  fnwe2lem3  39514  aomclem8  39523  brfvid  39894  brfvidRP  39895  brfvrcld  39898  brfvrcld2  39899  iunrelexpuztr  39926  brtrclfv2  39934  neicvgnvor  40328  neicvgel1  40331  fperdvper  42065  upwlkbprop  43842  rngcifuestrc  44097
  Copyright terms: Public domain W3C validator