Theorem breqd 5112

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561   class class class wbr 5101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-clel 2838  df-br 5102

This theorem is referenced by:  breq123d  5115  breqdi  5116  sbcbr123  5155  sbcbr  5156  sbcbr12g  5157  fvmptopab  7451  brfvopab  7453  mptmpoopabbrd  8062  mptmpoopabovd  8063  bropopvvv  8069  bropfvvvvlem  8070  sprmpod  8204  fprlem1  8281  supeq123d  9394  frrlem15  9713  fpwwe2lem11  10610  fpwwe2  10612  brtrclfv  15025  dfrtrclrec2  15081  rtrclreclem3  15083  relexpindlem  15086  shftfib  15095  2shfti  15103  prdsval  17494  pwsle  17532  pwsleval  17533  imasleval  17581  issect  17796  isinv  17803  brcic  17841  ciclcl  17845  cicrcl  17846  isfunc  17907  funcres2c  17946  isfull  17955  isfth  17959  fullpropd  17965  fthpropd  17966  elhoma  18075  isposd  18364  pltval  18372  lubfval  18390  glbfval  18403  joinfval  18413  meetfval  18427  odujoin  18448  odumeet  18450  resstos  18472  ipole  18576  eqgval  19228  isomnd  20173  submomnd  20182  ogrpaddltrd  20190  unitpropd  20476  rngcifuestrc  20699  isorng  20917  znleval  21613  ltbval  22103  opsrval  22106  lmbr  23325  metustexhalf  24623  metucn  24638  isphtpc  25063  taylthlem1  26443  ulmval  26450  tgjustf  28649  iscgrg  28688  legov  28761  ishlg  28778  opphllem5  28931  opphllem6  28932  hpgbr  28940  tgplnfn  28989  plngval  28991  isplng  28992  iscgra  29010  acopy  29034  isinag  29039  isleag  29048  iseqlg  29068  wlkonprop  29864  wksonproplem  29910  istrlson  29912  upgrwlkdvspth  29946  ispthson  29949  isspthson  29950  cyclispthon  30011  wspthsn  30055  wspthsnon  30059  iswspthsnon  30063  1pthon2v  30362  3wlkond  30380  dfconngr1  30397  isconngr  30398  isconngr1  30399  1conngr  30403  conngrv2edg  30404  minvecolem4b  31088  minvecolem4  31090  br8d  32816  ressprs  33150  mntoval  33166  mgcoval  33170  mgcval  33171  isinftm  33367  rprmval  33715  metidv  34191  pstmfval  34195  faeval  34545  brfae  34547  isacycgr  35500  isacycgr1  35501  issconn  35581  satfbrsuc  35721  mclsax  35924  weiunpo  36830  weiunfr  36832  bj-imdirval3  37681  unceq  38101  alrmomodm  38863  relbrcoss  39040  lcvbr  39650  isopos  39809  cmtvalN  39840  isoml  39867  cvrfval  39897  cvrval  39898  pats  39914  isatl  39928  iscvlat  39952  ishlat1  39981  llnset  40134  lplnset  40158  lvolset  40201  lineset  40367  psubspset  40373  pmapfval  40385  lautset  40711  ldilfset  40737  ltrnfset  40746  trlfset  40789  diaffval  41659  dicffval  41803  dihffval  41859  prjspnvs  43207  fnwe2lem2  43633  fnwe2lem3  43634  aomclem8  43643  brfvid  44268  brfvidRP  44269  brfvrcld  44272  brfvrcld2  44273  iunrelexpuztr  44300  brtrclfv2  44308  neicvgnvor  44697  neicvgel1  44700  fperdvper  46484  upwlkbprop  48751  isprsd  49567  lubeldm2d  49570  glbeldm2d  49571  catprsc  49625  catprsc2  49626  oppccicb  49663  funcoppc2  49755  uptpos  49810  prsthinc  50076  prstcle  50168  lanup  50253  ranup  50254  islmd  50277  cmddu  50280  lmdran  50283  cmdlan  50284