Theorem breqd 5163

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   class class class wbr 5152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2720  df-clel 2806  df-br 5153

This theorem is referenced by:  breq123d  5166  breqdi  5167  sbcbr123  5206  sbcbr  5207  sbcbr12g  5208  fvmptopab  7480  fvmptopabOLD  7481  brfvopab  7483  mptmpoopabbrd  8091  mptmpoopabbrdOLD  8092  mptmpoopabovd  8093  mptmpoopabbrdOLDOLD  8094  mptmpoopabovdOLD  8095  bropopvvv  8101  bropfvvvvlem  8102  sprmpod  8236  fprlem1  8312  wfrlem5OLD  8340  supeq123d  9481  frrlem15  9788  fpwwe2lem11  10672  fpwwe2  10674  brtrclfv  14989  dfrtrclrec2  15045  rtrclreclem3  15047  relexpindlem  15050  shftfib  15059  2shfti  15067  prdsval  17444  pwsle  17481  pwsleval  17482  imasleval  17530  issect  17743  isinv  17750  brcic  17788  ciclcl  17792  cicrcl  17793  isfunc  17857  funcres2c  17897  isfull  17906  isfth  17910  fullpropd  17916  fthpropd  17917  elhoma  18028  isposd  18322  pltval  18331  lubfval  18349  glbfval  18362  joinfval  18372  meetfval  18386  odujoin  18407  odumeet  18409  ipole  18533  eqgval  19139  unitpropd  20363  rngcifuestrc  20579  znleval  21495  ltbval  21988  opsrval  21991  lmbr  23182  metustexhalf  24485  metucn  24500  isphtpc  24940  taylthlem1  26328  ulmval  26336  tgjustf  28297  iscgrg  28336  legov  28409  ishlg  28426  opphllem5  28575  opphllem6  28576  hpgbr  28584  iscgra  28633  acopy  28657  isinag  28662  isleag  28671  iseqlg  28691  wlkonprop  29492  wksonproplem  29538  wksonproplemOLD  29539  istrlson  29541  upgrwlkdvspth  29573  ispthson  29576  isspthson  29577  cyclispthon  29635  wspthsn  29679  wspthsnon  29683  iswspthsnon  29687  1pthon2v  29983  3wlkond  30001  dfconngr1  30018  isconngr  30019  isconngr1  30020  1conngr  30024  conngrv2edg  30025  minvecolem4b  30708  minvecolem4  30710  br8d  32421  ressprs  32711  resstos  32715  mntoval  32730  mgcoval  32734  mgcval  32735  isomnd  32802  submomnd  32811  ogrpaddltrd  32820  isinftm  32910  isorng  33038  rprmval  33258  metidv  33526  pstmfval  33530  faeval  33898  brfae  33900  isacycgr  34788  isacycgr1  34789  issconn  34869  satfbrsuc  35009  mclsax  35212  bj-imdirval3  36696  unceq  37103  alrmomodm  37863  relbrcoss  37950  lcvbr  38525  isopos  38684  cmtvalN  38715  isoml  38742  cvrfval  38772  cvrval  38773  pats  38789  isatl  38803  iscvlat  38827  ishlat1  38856  llnset  39010  lplnset  39034  lvolset  39077  lineset  39243  psubspset  39249  pmapfval  39261  lautset  39587  ldilfset  39613  ltrnfset  39622  trlfset  39665  diaffval  40535  dicffval  40679  dihffval  40735  prjspnvs  42075  fnwe2lem2  42506  fnwe2lem3  42507  aomclem8  42516  brfvid  43148  brfvidRP  43149  brfvrcld  43152  brfvrcld2  43153  iunrelexpuztr  43180  brtrclfv2  43188  neicvgnvor  43577  neicvgel1  43580  fperdvper  45336  upwlkbprop  47278  isprsd  48052  lubeldm2d  48055  glbeldm2d  48056  catprsc  48097  catprsc2  48098  prsthinc  48138  prstcle  48154

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »