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

Theorem breqd 4822
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 4813 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652   class class class wbr 4811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-clel 2761  df-br 4812
This theorem is referenced by:  breq123d  4825  breqdi  4826  sbcbr123  4865  sbcbr  4866  sbcbr12g  4867  fvmptopab  6897  brfvopab  6900  mptmpt2opabbrd  7451  mptmpt2opabovd  7452  bropopvvv  7459  bropfvvvvlem  7460  sprmpt2d  7555  wfrlem5  7625  supeq123d  8565  fpwwe2lem12  9718  fpwwe2  9720  brtrclfv  14031  dfrtrclrec2  14085  rtrclreclem3  14088  relexpindlem  14091  shftfib  14100  2shfti  14108  prdsval  16384  pwsle  16421  pwsleval  16422  imasleval  16470  issect  16681  isinv  16688  episect  16713  brcic  16726  ciclcl  16730  cicrcl  16731  isfunc  16792  funcres2c  16829  isfull  16838  isfth  16842  fullpropd  16848  fthpropd  16849  elhoma  16950  isposd  17224  pltval  17229  lubfval  17247  glbfval  17260  joinfval  17270  meetfval  17284  odumeet  17409  odujoin  17411  ipole  17427  eqgval  17910  unitpropd  18967  ltbval  19748  opsrval  19751  znleval  20178  lmbr  21345  metustexhalf  22643  metucn  22658  isphtpc  23075  dvef  24037  taylthlem1  24421  ulmval  24428  iscgrg  25701  legov  25774  ishlg  25791  opphllem5  25937  opphllem6  25938  hpgbr  25946  iscgra  25995  acopy  26018  acopyeu  26019  isinag  26023  isleag  26027  iseqlg  26041  wlkonprop  26848  wksonproplem  26896  istrlson  26898  upgrwlkdvspth  26930  ispthson  26933  isspthson  26934  cyclispthon  26992  wspthsn  27037  wspthsnon  27041  iswspthsnon  27046  iswspthsnonOLD  27047  1pthon2v  27434  3wlkond  27452  dfconngr1  27469  isconngr  27470  isconngr1  27471  1conngr  27475  conngrv2edg  27476  minvecolem4b  28193  minvecolem4  28195  br8d  29873  ressprs  30105  resstos  30110  isomnd  30151  submomnd  30160  ogrpaddltrd  30170  isinftm  30185  isorng  30249  metidv  30385  pstmfval  30389  faeval  30759  brfae  30761  issconn  31659  mclsax  31917  frrlem5  32231  unceq  33813  alrmomodm  34556  relbrcoss  34628  lcvbr  34980  isopos  35139  cmtvalN  35170  isoml  35197  cvrfval  35227  cvrval  35228  pats  35244  isatl  35258  iscvlat  35282  ishlat1  35311  llnset  35464  lplnset  35488  lvolset  35531  lineset  35697  psubspset  35703  pmapfval  35715  lautset  36041  ldilfset  36067  ltrnfset  36076  trlfset  36119  diaffval  36989  dicffval  37133  dihffval  37189  fnwe2lem2  38301  fnwe2lem3  38302  aomclem8  38311  brfvid  38657  brfvidRP  38658  brfvrcld  38661  brfvrcld2  38662  iunrelexpuztr  38689  brtrclfv2  38697  neicvgnvor  39091  neicvgel1  39094  fperdvper  40774  upwlkbprop  42391  rngcifuestrc  42669
  Copyright terms: Public domain W3C validator