Theorem breqd 5076

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   class class class wbr 5065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-br 5066

This theorem is referenced by:  breq123d  5079  breqdi  5080  sbcbr123  5119  sbcbr  5120  sbcbr12g  5121  fvmptopab  7208  brfvopab  7210  mptmpoopabbrd  7777  mptmpoopabovd  7778  bropopvvv  7784  bropfvvvvlem  7785  sprmpod  7889  wfrlem5  7958  supeq123d  8913  fpwwe2lem12  10062  fpwwe2  10064  brtrclfv  14361  dfrtrclrec2  14415  rtrclreclem3  14418  relexpindlem  14421  shftfib  14430  2shfti  14438  prdsval  16727  pwsle  16764  pwsleval  16765  imasleval  16813  issect  17022  isinv  17029  brcic  17067  ciclcl  17071  cicrcl  17072  isfunc  17133  funcres2c  17170  isfull  17179  isfth  17183  fullpropd  17189  fthpropd  17190  elhoma  17291  isposd  17564  pltval  17569  lubfval  17587  glbfval  17600  joinfval  17610  meetfval  17624  odumeet  17749  odujoin  17751  ipole  17767  eqgval  18328  unitpropd  19446  ltbval  20251  opsrval  20254  znleval  20700  lmbr  21865  metustexhalf  23165  metucn  23180  isphtpc  23597  taylthlem1  24960  ulmval  24967  tgjustf  26258  iscgrg  26297  legov  26370  ishlg  26387  opphllem5  26536  opphllem6  26537  hpgbr  26545  iscgra  26594  acopy  26618  isinag  26623  isleag  26632  iseqlg  26652  wlkonprop  27439  wksonproplem  27485  istrlson  27487  upgrwlkdvspth  27519  ispthson  27522  isspthson  27523  cyclispthon  27581  wspthsn  27625  wspthsnon  27629  iswspthsnon  27633  1pthon2v  27931  3wlkond  27949  dfconngr1  27966  isconngr  27967  isconngr1  27968  1conngr  27972  conngrv2edg  27973  minvecolem4b  28654  minvecolem4  28656  br8d  30360  ressprs  30642  resstos  30647  isomnd  30702  submomnd  30711  ogrpaddltrd  30720  isinftm  30810  isorng  30872  metidv  31132  pstmfval  31136  faeval  31505  brfae  31507  isacycgr  32392  isacycgr1  32393  issconn  32473  satfbrsuc  32613  mclsax  32816  fprlem1  33137  frrlem15  33142  bj-imdirval3  34473  unceq  34868  alrmomodm  35612  relbrcoss  35685  lcvbr  36156  isopos  36315  cmtvalN  36346  isoml  36373  cvrfval  36403  cvrval  36404  pats  36420  isatl  36434  iscvlat  36458  ishlat1  36487  llnset  36640  lplnset  36664  lvolset  36707  lineset  36873  psubspset  36879  pmapfval  36891  lautset  37217  ldilfset  37243  ltrnfset  37252  trlfset  37295  diaffval  38165  dicffval  38309  dihffval  38365  fnwe2lem2  39649  fnwe2lem3  39650  aomclem8  39659  brfvid  40030  brfvidRP  40031  brfvrcld  40034  brfvrcld2  40035  iunrelexpuztr  40062  brtrclfv2  40070  neicvgnvor  40464  neicvgel1  40467  fperdvper  42201  upwlkbprop  44012  rngcifuestrc  44267