Theorem breqd 5113

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

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq 5104	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-br 5103

This theorem is used by:  breq123d  5116  breqdi  5117  sbcbr123  5158  sbcbr  5159  sbcbr12g  5160  fvmptopab  7463  brfvopab  7465  mptmpoopabbrd  8077  mptmpoopabovd  8078  bropopvvv  8084  bropfvvvvlem  8085  sprmpod  8219  fprlem1  8296  supeq123d  9420  frrlem15  9739  fpwwe2lem11  10697  fpwwe2  10699  brtrclfv  15122  dfrtrclrec2  15178  rtrclreclem3  15180  relexpindlem  15183  shftfib  15192  2shfti  15200  prdsval  17587  pwsle  17625  pwsleval  17626  imasleval  17674  issect  17889  isinv  17896  brcic  17934  ciclcl  17938  cicrcl  17939  isfunc  18000  funcres2c  18039  isfull  18048  isfth  18052  fullpropd  18058  fthpropd  18059  elhoma  18168  isposd  18457  pltval  18465  lubfval  18483  glbfval  18496  joinfval  18506  meetfval  18520  odujoin  18541  odumeet  18543  resstos  18565  ipole  18669  eqgval  19350  isomnd  20298  submomnd  20307  ogrpaddltrd  20315  unitpropd  20608  rngcifuestrc  20852  isorng  21079  znleval  21821  ltbval  22313  opsrval  22316  lmbr  23537  metustexhalf  24836  metucn  24851  isphtpc  25276  taylthlem1  26663  ulmval  26670  tgjustf  28868  iscgrg  28908  legov  28981  ishlg2  28998  ishlg  29001  opphllem5  29160  opphllem6  29161  hpgbr  29171  tgplnfn  29186  plngval  29188  isplng  29189  iscgra  29249  acopy  29274  isinag  29290  isleag  29299  cgrabasimass  29311  angmgmval  29327  iseqlg  29345  dfprlng3  29359  wlkonprop  30170  wksonproplem  30220  istrlson  30222  upgrwlkdvspth  30258  ispthson  30261  isspthson  30262  cyclispthon  30326  wspthsn  30370  wspthsnon  30374  iswspthsnon  30378  isacycgr  30684  isacycgr1  30685  1pthon2v  30687  3wlkond  30705  dfconngr1  30722  isconngr  30723  isconngr1  30724  1conngr  30728  conngrv2edg  30729  minvecolem4b  31413  minvecolem4  31415  br8d  33135  ressprs  33460  mntoval  33476  mgcoval  33480  mgcval  33481  isinftm  33675  rprmval  33981  metidv  34457  pstmfval  34461  faeval  34812  brfae  34814  issconn  35912  satfbrsuc  36052  mclsax  36255  weiunpo  37175  weiunfr  37177  bj-imdirval3  38025  unceq  38444  alrmomodm  39211  relbrcoss  39388  lcvbr  39998  isopos  40157  cmtvalN  40188  isoml  40215  cvrfval  40245  cvrval  40246  pats  40262  isatl  40276  iscvlat  40300  ishlat1  40329  llnset  40482  lplnset  40506  lvolset  40549  lineset  40715  psubspset  40721  pmapfval  40733  lautset  41059  ldilfset  41085  ltrnfset  41094  trlfset  41137  diaffval  42007  dicffval  42151  dihffval  42207  prjspnvs  43570  fnwe2lem2  43996  fnwe2lem3  43997  aomclem8  44006  brfvid  44631  brfvidRP  44632  brfvrcld  44635  brfvrcld2  44636  iunrelexpuztr  44663  brtrclfv2  44671  neicvgnvor  45060  neicvgel1  45063  fperdvper  46851  upwlkbprop  49158  isprsd  49985  lubeldm2d  49988  glbeldm2d  49989  catprsc  50043  catprsc2  50044  oppccicb  50081  funcoppc2  50173  uptpos  50228  prsthinc  50494  prstcle  50586  lanup  50671  ranup  50672  islmd  50695  cmddu  50698  lmdran  50701  cmdlan  50702