Theorem breqd 5160

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-br 5150

This theorem is referenced by:  breq123d  5163  breqdi  5164  sbcbr123  5203  sbcbr  5204  sbcbr12g  5205  fvmptopab  7463  fvmptopabOLD  7464  brfvopab  7466  mptmpoopabbrd  8067  mptmpoopabovd  8068  mptmpoopabbrdOLD  8069  mptmpoopabovdOLD  8070  bropopvvv  8076  bropfvvvvlem  8077  sprmpod  8209  fprlem1  8285  wfrlem5OLD  8313  supeq123d  9445  frrlem15  9752  fpwwe2lem11  10636  fpwwe2  10638  brtrclfv  14949  dfrtrclrec2  15005  rtrclreclem3  15007  relexpindlem  15010  shftfib  15019  2shfti  15027  prdsval  17401  pwsle  17438  pwsleval  17439  imasleval  17487  issect  17700  isinv  17707  brcic  17745  ciclcl  17749  cicrcl  17750  isfunc  17814  funcres2c  17852  isfull  17861  isfth  17865  fullpropd  17871  fthpropd  17872  elhoma  17982  isposd  18276  pltval  18285  lubfval  18303  glbfval  18316  joinfval  18326  meetfval  18340  odujoin  18361  odumeet  18363  ipole  18487  eqgval  19057  unitpropd  20231  znleval  21110  ltbval  21598  opsrval  21601  lmbr  22762  metustexhalf  24065  metucn  24080  isphtpc  24510  taylthlem1  25885  ulmval  25892  tgjustf  27724  iscgrg  27763  legov  27836  ishlg  27853  opphllem5  28002  opphllem6  28003  hpgbr  28011  iscgra  28060  acopy  28084  isinag  28089  isleag  28098  iseqlg  28118  wlkonprop  28915  wksonproplem  28961  wksonproplemOLD  28962  istrlson  28964  upgrwlkdvspth  28996  ispthson  28999  isspthson  29000  cyclispthon  29058  wspthsn  29102  wspthsnon  29106  iswspthsnon  29110  1pthon2v  29406  3wlkond  29424  dfconngr1  29441  isconngr  29442  isconngr1  29443  1conngr  29447  conngrv2edg  29448  minvecolem4b  30131  minvecolem4  30133  br8d  31839  ressprs  32133  resstos  32137  mntoval  32152  mgcoval  32156  mgcval  32157  isomnd  32219  submomnd  32228  ogrpaddltrd  32237  isinftm  32327  isorng  32417  rprmval  32633  metidv  32872  pstmfval  32876  faeval  33244  brfae  33246  isacycgr  34136  isacycgr1  34137  issconn  34217  satfbrsuc  34357  mclsax  34560  bj-imdirval3  36065  unceq  36465  alrmomodm  37228  relbrcoss  37316  lcvbr  37891  isopos  38050  cmtvalN  38081  isoml  38108  cvrfval  38138  cvrval  38139  pats  38155  isatl  38169  iscvlat  38193  ishlat1  38222  llnset  38376  lplnset  38400  lvolset  38443  lineset  38609  psubspset  38615  pmapfval  38627  lautset  38953  ldilfset  38979  ltrnfset  38988  trlfset  39031  diaffval  39901  dicffval  40045  dihffval  40101  prjspnvs  41362  fnwe2lem2  41793  fnwe2lem3  41794  aomclem8  41803  brfvid  42438  brfvidRP  42439  brfvrcld  42442  brfvrcld2  42443  iunrelexpuztr  42470  brtrclfv2  42478  neicvgnvor  42867  neicvgel1  42870  fperdvper  44635  upwlkbprop  46516  rngcifuestrc  46895  isprsd  47588  lubeldm2d  47591  glbeldm2d  47592  catprsc  47633  catprsc2  47634  prsthinc  47674  prstcle  47690