Theorem breqd 5103

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

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

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 5093

This theorem is referenced by:  breq123d  5106  breqdi  5107  sbcbr123  5146  sbcbr  5147  sbcbr12g  5148  fvmptopab  7404  brfvopab  7406  mptmpoopabbrd  8015  mptmpoopabbrdOLD  8016  mptmpoopabovd  8017  bropopvvv  8023  bropfvvvvlem  8024  sprmpod  8157  fprlem1  8233  supeq123d  9340  frrlem15  9653  fpwwe2lem11  10535  fpwwe2  10537  brtrclfv  14909  dfrtrclrec2  14965  rtrclreclem3  14967  relexpindlem  14970  shftfib  14979  2shfti  14987  prdsval  17359  pwsle  17396  pwsleval  17397  imasleval  17445  issect  17660  isinv  17667  brcic  17705  ciclcl  17709  cicrcl  17710  isfunc  17771  funcres2c  17810  isfull  17819  isfth  17823  fullpropd  17829  fthpropd  17830  elhoma  17939  isposd  18228  pltval  18236  lubfval  18254  glbfval  18267  joinfval  18277  meetfval  18291  odujoin  18312  odumeet  18314  resstos  18336  ipole  18440  eqgval  19056  isomnd  20002  submomnd  20011  ogrpaddltrd  20019  unitpropd  20302  rngcifuestrc  20524  isorng  20746  znleval  21461  ltbval  21948  opsrval  21951  lmbr  23143  metustexhalf  24442  metucn  24457  isphtpc  24891  taylthlem1  26279  ulmval  26287  tgjustf  28422  iscgrg  28461  legov  28534  ishlg  28551  opphllem5  28700  opphllem6  28701  hpgbr  28709  iscgra  28758  acopy  28782  isinag  28787  isleag  28796  iseqlg  28816  wlkonprop  29606  wksonproplem  29652  istrlson  29654  upgrwlkdvspth  29688  ispthson  29691  isspthson  29692  cyclispthon  29753  wspthsn  29797  wspthsnon  29801  iswspthsnon  29805  1pthon2v  30101  3wlkond  30119  dfconngr1  30136  isconngr  30137  isconngr1  30138  1conngr  30142  conngrv2edg  30143  minvecolem4b  30826  minvecolem4  30828  br8d  32560  ressprs  32917  mntoval  32933  mgcoval  32937  mgcval  32938  isinftm  33132  rprmval  33462  metidv  33875  pstmfval  33879  faeval  34229  brfae  34231  isacycgr  35138  isacycgr1  35139  issconn  35219  satfbrsuc  35359  mclsax  35562  weiunpo  36459  weiunfr  36461  bj-imdirval3  37178  unceq  37597  alrmomodm  38347  relbrcoss  38443  lcvbr  39020  isopos  39179  cmtvalN  39210  isoml  39237  cvrfval  39267  cvrval  39268  pats  39284  isatl  39298  iscvlat  39322  ishlat1  39351  llnset  39504  lplnset  39528  lvolset  39571  lineset  39737  psubspset  39743  pmapfval  39755  lautset  40081  ldilfset  40107  ltrnfset  40116  trlfset  40159  diaffval  41029  dicffval  41173  dihffval  41229  prjspnvs  42613  fnwe2lem2  43044  fnwe2lem3  43045  aomclem8  43054  brfvid  43680  brfvidRP  43681  brfvrcld  43684  brfvrcld2  43685  iunrelexpuztr  43712  brtrclfv2  43720  neicvgnvor  44109  neicvgel1  44112  fperdvper  45920  upwlkbprop  48142  isprsd  48959  lubeldm2d  48962  glbeldm2d  48963  catprsc  49018  catprsc2  49019  oppccicb  49056  funcoppc2  49148  uptpos  49203  prsthinc  49469  prstcle  49561  lanup  49646  ranup  49647  islmd  49670  cmddu  49673  lmdran  49676  cmdlan  49677