Theorem breqd 4594

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-br 4584

This theorem is referenced by:  breq123d  4597  breqdi  4598  sbcbr123  4636  sbcbr  4637  sbcbr12g  4638  fvmptopab1  6594  brfvopab  6598  bropopvvv  7142  bropfvvvvlem  7143  sprmpt2d  7237  wfrlem5  7306  supeq123d  8239  fpwwe2lem12  9342  fpwwe2  9344  brtrclfv  13591  dfrtrclrec2  13645  rtrclreclem3  13648  relexpindlem  13651  shftfib  13660  2shfti  13668  prdsval  15938  pwsle  15975  pwsleval  15976  imasleval  16024  issect  16236  isinv  16243  episect  16268  brcic  16281  ciclcl  16285  cicrcl  16286  isfunc  16347  funcres2c  16384  isfull  16393  isfth  16397  fullpropd  16403  fthpropd  16404  elhoma  16505  isposd  16778  pltval  16783  lubfval  16801  glbfval  16814  joinfval  16824  meetfval  16838  odumeet  16963  odujoin  16965  ipole  16981  eqgval  17466  unitpropd  18520  ltbval  19292  opsrval  19295  znleval  19722  lmbr  20872  metustexhalf  22171  metucn  22186  isphtpc  22601  dvef  23547  taylthlem1  23931  ulmval  23938  iscgrg  25207  legov  25280  ishlg  25297  opphllem5  25443  opphllem6  25444  hpgbr  25452  iscgra  25501  acopy  25524  acopyeu  25525  isinag  25529  isleag  25533  iseqlg  25547  wlkon  26061  iswlkon  26062  wlkonprop  26063  trls  26066  trlon  26070  istrlon  26071  trlonprop  26072  pths  26096  spths  26097  pthon  26105  ispthon  26106  pthonprop  26107  spthon  26112  isspthon  26113  spthonprp  26115  cyclispthon  26161  dfconngra1  26199  isconngra  26200  isconngra1  26201  1conngra  26203  clwlk  26281  clwlkcompim  26292  is2wlkonot  26390  is2spthonot  26391  2wlkonot  26392  2spthonot  26393  2wlkonot3v  26402  2spthonot3v  26403  iseupa  26492  minvecolem4b  27118  minvecolem4  27120  br8d  28802  ressprs  28986  resstos  28991  isomnd  29032  submomnd  29041  ogrpaddltrd  29051  isinftm  29066  isorng  29130  metidv  29263  pstmfval  29267  faeval  29636  brfae  29638  isscon  30462  mclsax  30720  frrlem5  31028  unceq  32556  lcvbr  33326  isopos  33485  cmtvalN  33516  isoml  33543  cvrfval  33573  cvrval  33574  pats  33590  isatl  33604  iscvlat  33628  ishlat1  33657  llnset  33809  lplnset  33833  lvolset  33876  lineset  34042  psubspset  34048  pmapfval  34060  lautset  34386  ldilfset  34412  ltrnfset  34421  trlfset  34465  diaffval  35337  dicffval  35481  dihffval  35537  fnwe2lem2  36639  fnwe2lem3  36640  aomclem8  36649  brfvid  36998  brfvidRP  36999  brfvrcld  37002  brfvrcld2  37003  iunrelexpuztr  37030  brtrclfv2  37038  neicvgnvor  37434  neicvgel1  37437  fperdvper  38808  mptmpt2opabbrd  40335  mptmpt2opabovd  40336  wlkbProp  40817  wlkOnprop  40866  1wlksonproplem  40912  istrlson  40914  upgrwlkdvspth  40945  ispthson  40948  isspthson  40949  cyclisPthon  41007  wspthsn  41046  wspthsnon  41050  iswspthsnon  41052  1pthon2v-av  41320  31wlkond  41338  dfconngr1  41355  isconngr  41356  isconngr1  41357  1conngr  41361  conngrv2edg  41362  rngcifuestrc  41789