Theorem breqd 5119

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   class class class wbr 5108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753  df-clel 2836  df-br 5109

This theorem is referenced by:  breq123d  5122  breqdi  5123  sbcbr123  5164  sbcbr  5165  sbcbr12g  5166  fvmptopab  7465  brfvopab  7467  mptmpoopabbrd  8077  mptmpoopabovd  8078  bropopvvv  8084  bropfvvvvlem  8085  sprmpod  8219  fprlem1  8296  supeq123d  9409  frrlem15  9728  fpwwe2lem11  10625  fpwwe2  10627  brtrclfv  15038  dfrtrclrec2  15094  rtrclreclem3  15096  relexpindlem  15099  shftfib  15108  2shfti  15116  prdsval  17507  pwsle  17545  pwsleval  17546  imasleval  17594  issect  17809  isinv  17816  brcic  17854  ciclcl  17858  cicrcl  17859  isfunc  17920  funcres2c  17959  isfull  17968  isfth  17972  fullpropd  17978  fthpropd  17979  elhoma  18088  isposd  18377  pltval  18385  lubfval  18403  glbfval  18416  joinfval  18426  meetfval  18440  odujoin  18461  odumeet  18463  resstos  18485  ipole  18589  eqgval  19244  isomnd  20192  submomnd  20201  ogrpaddltrd  20209  unitpropd  20498  rngcifuestrc  20723  isorng  20943  znleval  21683  ltbval  22173  opsrval  22176  lmbr  23394  metustexhalf  24692  metucn  24707  isphtpc  25132  taylthlem1  26512  ulmval  26519  tgjustf  28718  iscgrg  28757  legov  28830  ishlg2  28847  ishlg  28850  opphllem5  29007  opphllem6  29008  hpgbr  29017  tgplnfn  29031  plngval  29033  isplng  29034  iscgra  29093  acopy  29117  isinag  29128  isleag  29137  iseqlg  29157  dfprlng3  29171  wlkonprop  29972  wksonproplem  30018  istrlson  30020  upgrwlkdvspth  30054  ispthson  30057  isspthson  30058  cyclispthon  30119  wspthsn  30163  wspthsnon  30167  iswspthsnon  30171  1pthon2v  30470  3wlkond  30488  dfconngr1  30505  isconngr  30506  isconngr1  30507  1conngr  30511  conngrv2edg  30512  minvecolem4b  31196  minvecolem4  31198  br8d  32919  ressprs  33252  mntoval  33268  mgcoval  33272  mgcval  33273  isinftm  33467  rprmval  33772  metidv  34248  pstmfval  34252  faeval  34602  brfae  34604  isacycgr  35591  isacycgr1  35592  issconn  35672  satfbrsuc  35812  mclsax  36015  weiunpo  36920  weiunfr  36922  bj-imdirval3  37772  unceq  38192  alrmomodm  38954  relbrcoss  39131  lcvbr  39741  isopos  39900  cmtvalN  39931  isoml  39958  cvrfval  39988  cvrval  39989  pats  40005  isatl  40019  iscvlat  40043  ishlat1  40072  llnset  40225  lplnset  40249  lvolset  40292  lineset  40458  psubspset  40464  pmapfval  40476  lautset  40802  ldilfset  40828  ltrnfset  40837  trlfset  40880  diaffval  41750  dicffval  41894  dihffval  41950  prjspnvs  43300  fnwe2lem2  43726  fnwe2lem3  43727  aomclem8  43736  brfvid  44361  brfvidRP  44362  brfvrcld  44365  brfvrcld2  44366  iunrelexpuztr  44393  brtrclfv2  44401  neicvgnvor  44790  neicvgel1  44793  fperdvper  46581  upwlkbprop  48848  isprsd  49678  lubeldm2d  49681  glbeldm2d  49682  catprsc  49736  catprsc2  49737  oppccicb  49774  funcoppc2  49866  uptpos  49921  prsthinc  50187  prstcle  50279  lanup  50364  ranup  50365  islmd  50388  cmddu  50391  lmdran  50394  cmdlan  50395