Theorem breqd 5117

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 5108	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-br 5107

This theorem is used by:  breq123d  5120  breqdi  5121  sbcbr123  5163  sbcbr  5164  sbcbr12g  5165  fvmptopab  7498  brfvopab  7500  mptmpoopabbrd  8119  mptmpoopabovd  8120  bropopvvv  8126  bropfvvvvlem  8127  fnwe2lem3  8174  fnwe2lem4  8175  sprmpod  8269  fprlem1  8346  supeq123d  9469  frrlem15  9788  fpwwe2lem11  10753  fpwwe2  10755  brtrclfv  15184  dfrtrclrec2  15240  rtrclreclem3  15242  relexpindlem  15245  shftfib  15254  2shfti  15262  prdsval  17655  pwsle  17693  pwsleval  17694  imasleval  17742  issect  17957  isinv  17964  brcic  18002  ciclcl  18006  cicrcl  18007  isfunc  18068  funcres2c  18107  isfull  18116  isfth  18120  fullpropd  18126  fthpropd  18127  elhoma  18236  isposd  18525  pltval  18533  lubfval  18551  glbfval  18564  joinfval  18574  meetfval  18588  odujoin  18609  odumeet  18611  resstos  18633  ipole  18737  eqgval  19418  isomnd  20367  submomnd  20376  ogrpaddltrd  20384  unitpropd  20677  rngcifuestrc  20921  isorng  21148  znleval  21890  ltbval  22382  opsrval  22385  lmbr  23606  metustexhalf  24905  metucn  24920  isphtpc  25345  taylthlem1  26730  ulmval  26737  tgjustf  28965  iscgrg  29005  legov  29078  ishlg2  29095  ishlg  29098  opphllem5  29257  opphllem6  29258  hpgbr  29268  tgplnfn  29283  plngval  29285  isplng  29286  iscgra  29346  acopy  29371  isinag  29387  isleag  29396  cgrabasimass  29408  angmgmval  29424  iseqlg  29442  dfprlng3  29456  wlkonprop  30267  wksonproplem  30317  istrlson  30319  upgrwlkdvspth  30355  ispthson  30358  isspthson  30359  cyclispthon  30423  wspthsn  30467  wspthsnon  30471  iswspthsnon  30475  isacycgr  30781  isacycgr1  30782  1pthon2v  30784  3wlkond  30802  dfconngr1  30819  isconngr  30820  isconngr1  30821  1conngr  30825  conngrv2edg  30826  minvecolem4b  31510  minvecolem4  31512  br8d  33274  ressprs  33597  mntoval  33613  mgcoval  33617  mgcval  33618  isinftm  33812  rprmval  34118  metidv  34594  pstmfval  34598  faeval  34949  brfae  34951  onf1oracwevd  36052  issconn  36158  satfbrsuc  36298  mclsax  36501  weiunpo  37431  weiunfr  37433  bj-imdirval3  38297  unceq  38716  alrmomodm  39483  relbrcoss  39660  lcvbr  40270  isopos  40429  cmtvalN  40460  isoml  40487  cvrfval  40517  cvrval  40518  pats  40534  isatl  40548  iscvlat  40572  ishlat1  40601  llnset  40754  lplnset  40778  lvolset  40821  lineset  40987  psubspset  40993  pmapfval  41005  lautset  41331  ldilfset  41357  ltrnfset  41366  trlfset  41409  diaffval  42279  dicffval  42423  dihffval  42479  prjspnvs  43841  prjspnnorm  43854  aomclem8  44256  brfvid  44879  brfvidRP  44880  brfvrcld  44883  brfvrcld2  44884  iunrelexpuztr  44911  brtrclfv2  44919  neicvgnvor  45308  neicvgel1  45311  fperdvper  47134  upwlkbprop  49441  isprsd  50274  lubeldm2d  50277  glbeldm2d  50278  catprsc  50332  catprsc2  50333  oppccicb  50370  funcoppc2  50464  uptpos  50519  prsthinc  50804  prstcle  50899  lanup  51029  ranup  51030  islmd  51053  cmddu  51056  lmdran  51059  cmdlan  51060