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 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  breq123d  5116  breqdi  5117  sbcbr123  5159  sbcbr  5160  sbcbr12g  5161  fvmptopab  7475  brfvopab  7477  mptmpoopabbrd  8094  mptmpoopabovd  8095  bropopvvv  8101  bropfvvvvlem  8102  fnwe2lem3  8147  fnwe2lem4  8148  sprmpod  8241  fprlem1  8318  supeq123d  9442  frrlem15  9761  fpwwe2lem11  10726  fpwwe2  10728  brtrclfv  15155  dfrtrclrec2  15211  rtrclreclem3  15213  relexpindlem  15216  shftfib  15225  2shfti  15233  prdsval  17626  pwsle  17664  pwsleval  17665  imasleval  17713  issect  17928  isinv  17935  brcic  17973  ciclcl  17977  cicrcl  17978  isfunc  18039  funcres2c  18078  isfull  18087  isfth  18091  fullpropd  18097  fthpropd  18098  elhoma  18207  isposd  18496  pltval  18504  lubfval  18522  glbfval  18535  joinfval  18545  meetfval  18559  odujoin  18580  odumeet  18582  resstos  18604  ipole  18708  eqgval  19389  isomnd  20337  submomnd  20346  ogrpaddltrd  20354  unitpropd  20647  rngcifuestrc  20891  isorng  21118  znleval  21860  ltbval  22352  opsrval  22355  lmbr  23576  metustexhalf  24875  metucn  24890  isphtpc  25315  taylthlem1  26700  ulmval  26707  tgjustf  28935  iscgrg  28975  legov  29048  ishlg2  29065  ishlg  29068  opphllem5  29227  opphllem6  29228  hpgbr  29238  tgplnfn  29253  plngval  29255  isplng  29256  iscgra  29316  acopy  29341  isinag  29357  isleag  29366  cgrabasimass  29378  angmgmval  29394  iseqlg  29412  dfprlng3  29426  wlkonprop  30237  wksonproplem  30287  istrlson  30289  upgrwlkdvspth  30325  ispthson  30328  isspthson  30329  cyclispthon  30393  wspthsn  30437  wspthsnon  30441  iswspthsnon  30445  isacycgr  30751  isacycgr1  30752  1pthon2v  30754  3wlkond  30772  dfconngr1  30789  isconngr  30790  isconngr1  30791  1conngr  30795  conngrv2edg  30796  minvecolem4b  31480  minvecolem4  31482  br8d  33244  ressprs  33569  mntoval  33585  mgcoval  33589  mgcval  33590  isinftm  33784  rprmval  34090  metidv  34566  pstmfval  34570  faeval  34921  brfae  34923  issconn  36033  satfbrsuc  36173  mclsax  36376  weiunpo  37295  weiunfr  37297  bj-imdirval3  38148  unceq  38567  alrmomodm  39334  relbrcoss  39511  lcvbr  40121  isopos  40280  cmtvalN  40311  isoml  40338  cvrfval  40368  cvrval  40369  pats  40385  isatl  40399  iscvlat  40423  ishlat1  40452  llnset  40605  lplnset  40629  lvolset  40672  lineset  40838  psubspset  40844  pmapfval  40856  lautset  41182  ldilfset  41208  ltrnfset  41217  trlfset  41260  diaffval  42130  dicffval  42274  dihffval  42330  prjspnvs  43691  prjspnnorm  43704  aomclem8  44106  brfvid  44730  brfvidRP  44731  brfvrcld  44734  brfvrcld2  44735  iunrelexpuztr  44762  brtrclfv2  44770  neicvgnvor  45159  neicvgel1  45162  fperdvper  46972  upwlkbprop  49279  isprsd  50106  lubeldm2d  50109  glbeldm2d  50110  catprsc  50164  catprsc2  50165  oppccicb  50202  funcoppc2  50294  uptpos  50349  prsthinc  50615  prstcle  50707  lanup  50792  ranup  50793  islmd  50816  cmddu  50819  lmdran  50822  cmdlan  50823