Theorem breq1d 4093

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breq1d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq1 4086	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   class class class wbr 4083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  eqnbrtrd  4101  eqbrtrd  4105  eqbrtrdi  4122  sbcbr2g  4141  pofun  4403  fmptco  5803  isorel  5938  isocnv  5941  isotr  5946  imbrov2fvoveq  6032  caovordig  6177  caovordg  6179  caovord  6183  xporderlem  6383  reldmtpos  6405  brtposg  6406  tpostpos  6416  tposoprab  6432  th3qlem2  6793  ensn1g  6957  fndmeng  6971  xpsneng  6989  xpcomco  6993  snnen2oprc  7029  tridc  7070  fimax2gtrilemstep  7071  unsnfidcel  7094  pm54.43  7374  pr1or2  7378  ccfunen  7461  ltsonq  7596  ltanqg  7598  ltmnqg  7599  archnqq  7615  prloc  7689  addnqprulem  7726  appdivnq  7761  mulnqpru  7767  mullocprlem  7768  1idpru  7789  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  caucvgprprlem1  7907  caucvgprprlem2  7908  ltsosr  7962  ltasrg  7968  addgt0sr  7973  mulextsr1  7979  prsrlt  7985  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  ltpsrprg  8001  pitonnlem2  8045  pitonn  8046  recidpipr  8054  axpre-ltadd  8084  axpre-mulext  8086  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  ltaddnegr  8583  ltsubadd  8590  lesubadd  8592  ltaddsub2  8595  leaddsub2  8597  ltaddpos  8610  lesub2  8615  ltsub2  8617  ltnegcon2  8622  lenegcon2  8625  addge01  8630  subge0  8633  suble0  8634  lesub0  8637  ltordlem  8640  apreap  8745  divap0b  8841  mulgt1  9021  ltmulgt11  9022  gt0div  9028  ge0div  9029  ltmuldiv  9032  ltmuldiv2  9033  lemuldiv2  9040  ltrec  9041  lerec2  9047  ltdiv23  9050  lediv23  9051  sup3exmid  9115  addltmul  9359  avglt1  9361  avgle1  9363  div4p1lem1div2  9376  ztri3or  9500  zlem1lt  9514  zgt0ge1  9516  qapne  9846  irrmulap  9855  divlt1lt  9932  divle1le  9933  xrltso  10004  xltnegi  10043  xltadd1  10084  xposdif  10090  xlesubadd  10091  xleaddadd  10095  nn0disj  10346  qavgle  10490  fldiv4lem1div2uz2  10538  frec2uzf1od  10640  iseqf1olemfvp  10744  seqf1oglem1  10753  exp3vallem  10774  expap0  10803  leexp2r  10827  sqap0  10840  nn0ltexp2  10943  nn0opthlem1d  10954  hashennnuni  11013  hashunlem  11038  zfz1isolemiso  11074  seq3coll  11077  swrdccatin2  11276  shftfvalg  11344  shftfibg  11346  shftfval  11347  shftfib  11349  shftfn  11350  2shfti  11357  shftidt2  11358  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemdecn  11538  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemsqa  11550  resqrexlemex  11551  abs00ap  11588  absdiflt  11618  absdifle  11619  lenegsq  11621  cau3lem  11640  minmax  11756  xrmaxltsup  11784  xrminmax  11791  xrltmininf  11796  xrlemininf  11797  clim  11807  clim2  11809  clim0  11811  clim0c  11812  climi0  11815  climuni  11819  2clim  11827  climshftlemg  11828  climshft  11830  climabs0  11833  climcn1  11834  climcn2  11835  addcn2  11836  subcn2  11837  mulcn2  11838  iser3shft  11872  climcau  11873  serf0  11878  sumeq1  11881  sumeq2  11885  sumrbdc  11905  summodclem2  11908  summodc  11909  zsumdc  11910  isumshft  12016  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodfap0  12071  prodfrecap  12072  prodfdivap  12073  ntrivcvgap  12074  ntrivcvgap0  12075  prodeq1f  12078  prodeq2w  12082  prodeq2  12083  prodrbdclem2  12099  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodntrivap  12110  fprodap0  12147  fprodrec  12155  fproddivapf  12157  fprodap0f  12162  tanaddaplem  12264  sin01bnd  12283  cos01bnd  12284  halfleoddlt  12420  gcddvds  12499  dvdssq  12567  lcmgcdlem  12614  lcmdvds  12616  isprm  12646  prmgt1  12669  isprm5lem  12678  isprm6  12684  pw2dvdslemn  12702  pw2dvdseu  12705  oddpwdclemxy  12706  oddpwdclemndvds  12708  oddpwdclemodd  12709  odzdvds  12783  pclem0  12824  pclemub  12825  pclemdc  12826  pcprecl  12827  pcprendvds  12828  pcpremul  12831  pceulem  12832  pcval  12834  pcelnn  12859  pc2dvds  12868  pcadd  12878  pcadd2  12879  pcmpt  12881  prmpwdvds  12893  4sqlem17  12945  imasaddfnlemg  13362  znf1o  14630  znidomb  14637  mplsubgfilemm  14677  mplsubgfilemcl  14678  blfvalps  15074  elblps  15079  elbl  15080  elbl3ps  15083  elbl3  15084  blres  15123  comet  15188  bdbl  15192  xmetxp  15196  xmetxpbl  15197  metcnp2  15202  txmetcnp  15207  cnbl0  15223  cnblcld  15224  bl2ioo  15239  addcncntoplem  15250  divcnap  15254  mpomulcn  15255  elcncf  15262  elcncf2  15263  cncfi  15267  rescncf  15270  mulc1cncf  15278  cncfco  15280  cncfmet  15281  cncfmptid  15286  addccncf  15289  cdivcncfap  15293  negcncf  15294  mulcncflem  15296  mulcncf  15297  ivthinclemlm  15323  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemdisj  15329  ivthinclemloc  15330  ivthinc  15332  ivthreinc  15334  limccl  15348  ellimc3apf  15349  limcdifap  15351  limcmpted  15352  limcimolemlt  15353  limcresi  15355  cnplimcim  15356  limccnpcntop  15364  limccnp2lem  15365  limccoap  15367  dvcoapbr  15396  dveflem  15415  eflt  15464  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  logltb  15563  logge0b  15579  loggt0b  15580  lgslem2  15695  lgslem3  15696  lgsval  15698  lgsfcl2  15700  lgsfle1  15703  lgsle1  15709  lgsdirprm  15728  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  vtxdumgrfival  16057  qdencn  16455  trilpolemlt1  16469