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

Theorem breqd 5068
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 5059 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷𝐶𝐵𝐷))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-br 5058
This theorem is referenced by:  breq123d  5071  breqdi  5072  sbcbr123  5111  sbcbr  5112  sbcbr12g  5113  fvmptopab  7198  brfvopab  7200  mptmpoopabbrd  7767  mptmpoopabovd  7768  bropopvvv  7774  bropfvvvvlem  7775  sprmpod  7879  wfrlem5  7948  supeq123d  8902  fpwwe2lem12  10051  fpwwe2  10053  brtrclfv  14350  dfrtrclrec2  14404  rtrclreclem3  14407  relexpindlem  14410  shftfib  14419  2shfti  14427  prdsval  16716  pwsle  16753  pwsleval  16754  imasleval  16802  issect  17011  isinv  17018  brcic  17056  ciclcl  17060  cicrcl  17061  isfunc  17122  funcres2c  17159  isfull  17168  isfth  17172  fullpropd  17178  fthpropd  17179  elhoma  17280  isposd  17553  pltval  17558  lubfval  17576  glbfval  17589  joinfval  17599  meetfval  17613  odumeet  17738  odujoin  17740  ipole  17756  eqgval  18267  unitpropd  19376  ltbval  20180  opsrval  20183  znleval  20629  lmbr  21794  metustexhalf  23093  metucn  23108  isphtpc  23525  taylthlem1  24888  ulmval  24895  tgjustf  26186  iscgrg  26225  legov  26298  ishlg  26315  opphllem5  26464  opphllem6  26465  hpgbr  26473  iscgra  26522  acopy  26546  isinag  26551  isleag  26560  iseqlg  26580  wlkonprop  27367  wksonproplem  27413  istrlson  27415  upgrwlkdvspth  27447  ispthson  27450  isspthson  27451  cyclispthon  27509  wspthsn  27553  wspthsnon  27557  iswspthsnon  27561  1pthon2v  27859  3wlkond  27877  dfconngr1  27894  isconngr  27895  isconngr1  27896  1conngr  27900  conngrv2edg  27901  minvecolem4b  28582  minvecolem4  28584  br8d  30289  ressprs  30569  resstos  30574  isomnd  30629  submomnd  30638  ogrpaddltrd  30647  isinftm  30737  isorng  30799  metidv  31031  pstmfval  31035  faeval  31404  brfae  31406  isacycgr  32289  isacycgr1  32290  issconn  32370  satfbrsuc  32510  mclsax  32713  fprlem1  33034  frrlem15  33039  bj-imdirval3  34366  unceq  34750  alrmomodm  35494  relbrcoss  35566  lcvbr  36037  isopos  36196  cmtvalN  36227  isoml  36254  cvrfval  36284  cvrval  36285  pats  36301  isatl  36315  iscvlat  36339  ishlat1  36368  llnset  36521  lplnset  36545  lvolset  36588  lineset  36754  psubspset  36760  pmapfval  36772  lautset  37098  ldilfset  37124  ltrnfset  37133  trlfset  37176  diaffval  38046  dicffval  38190  dihffval  38246  fnwe2lem2  39529  fnwe2lem3  39530  aomclem8  39539  brfvid  39910  brfvidRP  39911  brfvrcld  39914  brfvrcld2  39915  iunrelexpuztr  39942  brtrclfv2  39950  neicvgnvor  40344  neicvgel1  40347  fperdvper  42079  upwlkbprop  43890  rngcifuestrc  44196
  Copyright terms: Public domain W3C validator