Theorem breqd 5118

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-br 5108

This theorem is used by:  breq123d  5121  breqdi  5122  sbcbr123  5163  sbcbr  5164  sbcbr12g  5165  fvmptopab  7471  brfvopab  7473  mptmpoopabbrd  8083  mptmpoopabovd  8084  bropopvvv  8090  bropfvvvvlem  8091  sprmpod  8225  fprlem1  8302  supeq123d  9423  frrlem15  9742  fpwwe2lem11  10653  fpwwe2  10655  brtrclfv  15077  dfrtrclrec2  15133  rtrclreclem3  15135  relexpindlem  15138  shftfib  15147  2shfti  15155  prdsval  17544  pwsle  17582  pwsleval  17583  imasleval  17631  issect  17846  isinv  17853  brcic  17891  ciclcl  17895  cicrcl  17896  isfunc  17957  funcres2c  17996  isfull  18005  isfth  18009  fullpropd  18015  fthpropd  18016  elhoma  18125  isposd  18414  pltval  18422  lubfval  18440  glbfval  18453  joinfval  18463  meetfval  18477  odujoin  18498  odumeet  18500  resstos  18522  ipole  18626  eqgval  19303  isomnd  20251  submomnd  20260  ogrpaddltrd  20268  unitpropd  20559  rngcifuestrc  20802  isorng  21028  znleval  21768  ltbval  22260  opsrval  22263  lmbr  23484  metustexhalf  24783  metucn  24798  isphtpc  25223  taylthlem1  26606  ulmval  26613  tgjustf  28812  iscgrg  28852  legov  28925  ishlg2  28942  ishlg  28945  opphllem5  29104  opphllem6  29105  hpgbr  29115  tgplnfn  29130  plngval  29132  isplng  29133  iscgra  29193  acopy  29218  isinag  29234  isleag  29243  iseqlg  29277  dfprlng3  29291  wlkonprop  30102  wksonproplem  30152  istrlson  30154  upgrwlkdvspth  30190  ispthson  30193  isspthson  30194  cyclispthon  30258  wspthsn  30302  wspthsnon  30306  iswspthsnon  30310  isacycgr  30616  isacycgr1  30617  1pthon2v  30619  3wlkond  30637  dfconngr1  30654  isconngr  30655  isconngr1  30656  1conngr  30660  conngrv2edg  30661  minvecolem4b  31345  minvecolem4  31347  br8d  33068  ressprs  33393  mntoval  33409  mgcoval  33413  mgcval  33414  isinftm  33608  rprmval  33913  metidv  34389  pstmfval  34393  faeval  34744  brfae  34746  issconn  35792  satfbrsuc  35932  mclsax  36135  weiunpo  37071  weiunfr  37073  bj-imdirval3  37923  unceq  38342  alrmomodm  39094  relbrcoss  39271  lcvbr  39881  isopos  40040  cmtvalN  40071  isoml  40098  cvrfval  40128  cvrval  40129  pats  40145  isatl  40159  iscvlat  40183  ishlat1  40212  llnset  40365  lplnset  40389  lvolset  40432  lineset  40598  psubspset  40604  pmapfval  40616  lautset  40942  ldilfset  40968  ltrnfset  40977  trlfset  41020  diaffval  41890  dicffval  42034  dihffval  42090  prjspnvs  43453  fnwe2lem2  43879  fnwe2lem3  43880  aomclem8  43889  brfvid  44514  brfvidRP  44515  brfvrcld  44518  brfvrcld2  44519  iunrelexpuztr  44546  brtrclfv2  44554  neicvgnvor  44943  neicvgel1  44946  fperdvper  46734  upwlkbprop  49041  isprsd  49868  lubeldm2d  49871  glbeldm2d  49872  catprsc  49926  catprsc2  49927  oppccicb  49964  funcoppc2  50056  uptpos  50111  prsthinc  50377  prstcle  50469  lanup  50554  ranup  50555  islmd  50578  cmddu  50581  lmdran  50584  cmdlan  50585