Theorem breqd 5154

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-br 5144

This theorem is referenced by:  breq123d  5157  breqdi  5158  sbcbr123  5197  sbcbr  5198  sbcbr12g  5199  fvmptopab  7487  fvmptopabOLD  7488  brfvopab  7490  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabovd  8107  mptmpoopabbrdOLDOLD  8108  mptmpoopabovdOLD  8109  bropopvvv  8115  bropfvvvvlem  8116  sprmpod  8249  fprlem1  8325  wfrlem5OLD  8353  supeq123d  9490  frrlem15  9797  fpwwe2lem11  10681  fpwwe2  10683  brtrclfv  15041  dfrtrclrec2  15097  rtrclreclem3  15099  relexpindlem  15102  shftfib  15111  2shfti  15119  prdsval  17500  pwsle  17537  pwsleval  17538  imasleval  17586  issect  17797  isinv  17804  brcic  17842  ciclcl  17846  cicrcl  17847  isfunc  17909  funcres2c  17948  isfull  17957  isfth  17961  fullpropd  17967  fthpropd  17968  elhoma  18077  isposd  18368  pltval  18377  lubfval  18395  glbfval  18408  joinfval  18418  meetfval  18432  odujoin  18453  odumeet  18455  ipole  18579  eqgval  19195  unitpropd  20417  rngcifuestrc  20639  znleval  21573  ltbval  22061  opsrval  22064  lmbr  23266  metustexhalf  24569  metucn  24584  isphtpc  25026  taylthlem1  26415  ulmval  26423  tgjustf  28481  iscgrg  28520  legov  28593  ishlg  28610  opphllem5  28759  opphllem6  28760  hpgbr  28768  iscgra  28817  acopy  28841  isinag  28846  isleag  28855  iseqlg  28875  wlkonprop  29676  wksonproplem  29722  wksonproplemOLD  29723  istrlson  29725  upgrwlkdvspth  29759  ispthson  29762  isspthson  29763  cyclispthon  29824  wspthsn  29868  wspthsnon  29872  iswspthsnon  29876  1pthon2v  30172  3wlkond  30190  dfconngr1  30207  isconngr  30208  isconngr1  30209  1conngr  30213  conngrv2edg  30214  minvecolem4b  30897  minvecolem4  30899  br8d  32622  ressprs  32954  resstos  32957  mntoval  32972  mgcoval  32976  mgcval  32977  isomnd  33078  submomnd  33087  ogrpaddltrd  33096  isinftm  33188  isorng  33329  rprmval  33544  metidv  33891  pstmfval  33895  faeval  34247  brfae  34249  isacycgr  35150  isacycgr1  35151  issconn  35231  satfbrsuc  35371  mclsax  35574  weiunpo  36466  weiunfr  36468  bj-imdirval3  37185  unceq  37604  alrmomodm  38360  relbrcoss  38447  lcvbr  39022  isopos  39181  cmtvalN  39212  isoml  39239  cvrfval  39269  cvrval  39270  pats  39286  isatl  39300  iscvlat  39324  ishlat1  39353  llnset  39507  lplnset  39531  lvolset  39574  lineset  39740  psubspset  39746  pmapfval  39758  lautset  40084  ldilfset  40110  ltrnfset  40119  trlfset  40162  diaffval  41032  dicffval  41176  dihffval  41232  prjspnvs  42630  fnwe2lem2  43063  fnwe2lem3  43064  aomclem8  43073  brfvid  43700  brfvidRP  43701  brfvrcld  43704  brfvrcld2  43705  iunrelexpuztr  43732  brtrclfv2  43740  neicvgnvor  44129  neicvgel1  44132  fperdvper  45934  upwlkbprop  48054  isprsd  48852  lubeldm2d  48855  glbeldm2d  48856  catprsc  48902  catprsc2  48903  prsthinc  49111  prstcle  49159