Theorem breqd 5130

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-br 5120

This theorem is referenced by:  breq123d  5133  breqdi  5134  sbcbr123  5173  sbcbr  5174  sbcbr12g  5175  fvmptopab  7461  fvmptopabOLD  7462  brfvopab  7464  mptmpoopabbrd  8079  mptmpoopabbrdOLD  8080  mptmpoopabovd  8081  mptmpoopabbrdOLDOLD  8082  mptmpoopabovdOLD  8083  bropopvvv  8089  bropfvvvvlem  8090  sprmpod  8223  fprlem1  8299  wfrlem5OLD  8327  supeq123d  9462  frrlem15  9771  fpwwe2lem11  10655  fpwwe2  10657  brtrclfv  15021  dfrtrclrec2  15077  rtrclreclem3  15079  relexpindlem  15082  shftfib  15091  2shfti  15099  prdsval  17469  pwsle  17506  pwsleval  17507  imasleval  17555  issect  17766  isinv  17773  brcic  17811  ciclcl  17815  cicrcl  17816  isfunc  17877  funcres2c  17916  isfull  17925  isfth  17929  fullpropd  17935  fthpropd  17936  elhoma  18045  isposd  18334  pltval  18342  lubfval  18360  glbfval  18373  joinfval  18383  meetfval  18397  odujoin  18418  odumeet  18420  ipole  18544  eqgval  19160  unitpropd  20377  rngcifuestrc  20599  znleval  21515  ltbval  22001  opsrval  22004  lmbr  23196  metustexhalf  24495  metucn  24510  isphtpc  24944  taylthlem1  26333  ulmval  26341  tgjustf  28452  iscgrg  28491  legov  28564  ishlg  28581  opphllem5  28730  opphllem6  28731  hpgbr  28739  iscgra  28788  acopy  28812  isinag  28817  isleag  28826  iseqlg  28846  wlkonprop  29638  wksonproplem  29684  wksonproplemOLD  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  32944  resstos  32947  mntoval  32962  mgcoval  32966  mgcval  32967  isomnd  33069  submomnd  33078  ogrpaddltrd  33087  isinftm  33179  isorng  33321  rprmval  33531  metidv  33923  pstmfval  33927  faeval  34277  brfae  34279  isacycgr  35167  isacycgr1  35168  issconn  35248  satfbrsuc  35388  mclsax  35591  weiunpo  36483  weiunfr  36485  bj-imdirval3  37202  unceq  37621  alrmomodm  38377  relbrcoss  38464  lcvbr  39039  isopos  39198  cmtvalN  39229  isoml  39256  cvrfval  39286  cvrval  39287  pats  39303  isatl  39317  iscvlat  39341  ishlat1  39370  llnset  39524  lplnset  39548  lvolset  39591  lineset  39757  psubspset  39763  pmapfval  39775  lautset  40101  ldilfset  40127  ltrnfset  40136  trlfset  40179  diaffval  41049  dicffval  41193  dihffval  41249  prjspnvs  42643  fnwe2lem2  43075  fnwe2lem3  43076  aomclem8  43085  brfvid  43711  brfvidRP  43712  brfvrcld  43715  brfvrcld2  43716  iunrelexpuztr  43743  brtrclfv2  43751  neicvgnvor  44140  neicvgel1  44143  fperdvper  45948  upwlkbprop  48113  isprsd  48929  lubeldm2d  48932  glbeldm2d  48933  catprsc  48988  catprsc2  48989  oppccicb  49018  funcoppc2  49086  uptpos  49131  prsthinc  49350  prstcle  49433  lanup  49515  ranup  49516  islmd  49535