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 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5103

This theorem is referenced by:  breq123d  5116  breqdi  5117  sbcbr123  5156  sbcbr  5157  sbcbr12g  5158  fvmptopab  7425  brfvopab  7427  mptmpoopabbrd  8039  mptmpoopabbrdOLD  8040  mptmpoopabovd  8041  bropopvvv  8047  bropfvvvvlem  8048  sprmpod  8181  fprlem1  8257  supeq123d  9378  frrlem15  9689  fpwwe2lem11  10573  fpwwe2  10575  brtrclfv  14946  dfrtrclrec2  15002  rtrclreclem3  15004  relexpindlem  15007  shftfib  15016  2shfti  15024  prdsval  17396  pwsle  17433  pwsleval  17434  imasleval  17482  issect  17697  isinv  17704  brcic  17742  ciclcl  17746  cicrcl  17747  isfunc  17808  funcres2c  17847  isfull  17856  isfth  17860  fullpropd  17866  fthpropd  17867  elhoma  17976  isposd  18265  pltval  18273  lubfval  18291  glbfval  18304  joinfval  18314  meetfval  18328  odujoin  18349  odumeet  18351  resstos  18373  ipole  18477  eqgval  19093  isomnd  20039  submomnd  20048  ogrpaddltrd  20056  unitpropd  20339  rngcifuestrc  20561  isorng  20783  znleval  21498  ltbval  21985  opsrval  21988  lmbr  23180  metustexhalf  24479  metucn  24494  isphtpc  24928  taylthlem1  26316  ulmval  26324  tgjustf  28455  iscgrg  28494  legov  28567  ishlg  28584  opphllem5  28733  opphllem6  28734  hpgbr  28742  iscgra  28791  acopy  28815  isinag  28820  isleag  28829  iseqlg  28849  wlkonprop  29639  wksonproplem  29685  istrlson  29687  upgrwlkdvspth  29721  ispthson  29724  isspthson  29725  cyclispthon  29786  wspthsn  29830  wspthsnon  29834  iswspthsnon  29838  1pthon2v  30134  3wlkond  30152  dfconngr1  30169  isconngr  30170  isconngr1  30171  1conngr  30175  conngrv2edg  30176  minvecolem4b  30859  minvecolem4  30861  br8d  32590  ressprs  32940  mntoval  32956  mgcoval  32960  mgcval  32961  isinftm  33152  rprmval  33482  metidv  33877  pstmfval  33881  faeval  34231  brfae  34233  isacycgr  35127  isacycgr1  35128  issconn  35208  satfbrsuc  35348  mclsax  35551  weiunpo  36448  weiunfr  36450  bj-imdirval3  37167  unceq  37586  alrmomodm  38336  relbrcoss  38432  lcvbr  39009  isopos  39168  cmtvalN  39199  isoml  39226  cvrfval  39256  cvrval  39257  pats  39273  isatl  39287  iscvlat  39311  ishlat1  39340  llnset  39494  lplnset  39518  lvolset  39561  lineset  39727  psubspset  39733  pmapfval  39745  lautset  40071  ldilfset  40097  ltrnfset  40106  trlfset  40149  diaffval  41019  dicffval  41163  dihffval  41219  prjspnvs  42603  fnwe2lem2  43035  fnwe2lem3  43036  aomclem8  43045  brfvid  43671  brfvidRP  43672  brfvrcld  43675  brfvrcld2  43676  iunrelexpuztr  43703  brtrclfv2  43711  neicvgnvor  44100  neicvgel1  44103  fperdvper  45912  upwlkbprop  48121  isprsd  48938  lubeldm2d  48941  glbeldm2d  48942  catprsc  48997  catprsc2  48998  oppccicb  49035  funcoppc2  49127  uptpos  49182  prsthinc  49448  prstcle  49540  lanup  49625  ranup  49626  islmd  49649  cmddu  49652  lmdran  49655  cmdlan  49656