Theorem breq1d 3885

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299   class class class wbr 3875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876

This theorem is referenced by:  eqbrtrd  3895  syl6eqbr  3912  sbcbr2g  3927  pofun  4172  fmptco  5518  isorel  5641  isocnv  5644  isotr  5649  imbrov2fvoveq  5731  caovordig  5868  caovordg  5870  caovord  5874  xporderlem  6058  reldmtpos  6080  brtposg  6081  tpostpos  6091  tposoprab  6107  th3qlem2  6462  ensn1g  6621  fndmeng  6634  xpsneng  6645  xpcomco  6649  snnen2oprc  6683  tridc  6722  fimax2gtrilemstep  6723  unsnfidcel  6738  pm54.43  6957  ltsonq  7107  ltanqg  7109  ltmnqg  7110  archnqq  7126  prloc  7200  addnqprulem  7237  appdivnq  7272  mulnqpru  7278  mullocprlem  7279  1idpru  7300  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdfl  7364  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlem2  7369  cauappcvgprlemlim  7370  cauappcvgpr  7371  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem1  7388  caucvgprlem2  7389  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemelu  7395  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnkltj  7398  caucvgprprlemnkeqj  7399  caucvgprprlemnbj  7402  caucvgprprlemml  7403  caucvgprprlemmu  7404  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexbt  7415  caucvgprprlemexb  7416  caucvgprprlemaddq  7417  caucvgprprlem1  7418  caucvgprprlem2  7419  ltsosr  7460  ltasrg  7466  addgt0sr  7471  mulextsr1  7476  prsrlt  7482  caucvgsrlemgt1  7490  caucvgsrlemoffres  7495  caucvgsr  7497  pitonnlem2  7534  pitonn  7535  recidpipr  7543  axpre-ltadd  7571  axpre-mulext  7573  nntopi  7579  axcaucvglemval  7582  axcaucvglemcau  7583  axcaucvglemres  7584  ltaddnegr  8054  ltsubadd  8061  lesubadd  8063  ltaddsub2  8066  leaddsub2  8068  ltaddpos  8081  lesub2  8086  ltsub2  8088  ltnegcon2  8093  lenegcon2  8096  addge01  8101  subge0  8104  suble0  8105  lesub0  8108  ltordlem  8111  apreap  8215  divap0b  8304  mulgt1  8479  ltmulgt11  8480  gt0div  8486  ge0div  8487  ltmuldiv  8490  ltmuldiv2  8491  lemuldiv2  8498  ltrec  8499  lerec2  8505  ltdiv23  8508  lediv23  8509  sup3exmid  8573  addltmul  8808  avglt1  8810  avgle1  8812  div4p1lem1div2  8825  ztri3or  8949  zlem1lt  8962  zgt0ge1  8964  qapne  9281  divlt1lt  9358  divle1le  9359  xrltso  9423  xltnegi  9459  xltadd1  9500  xposdif  9506  xlesubadd  9507  xleaddadd  9511  nn0disj  9756  qavgle  9877  frec2uzf1od  10020  iseqf1olemfvp  10111  exp3vallem  10135  expap0  10164  leexp2r  10188  sqap0  10200  nn0opthlem1d  10307  hashennnuni  10366  hashunlem  10391  zfz1isolemiso  10423  seq3coll  10426  shftfvalg  10431  shftfibg  10433  shftfval  10434  shftfib  10436  shftfn  10437  2shfti  10444  shftidt2  10445  caucvgre  10593  cvg1nlemcau  10596  cvg1nlemres  10597  resqrexlemdecn  10624  resqrexlemoverl  10633  resqrexlemglsq  10634  resqrexlemsqa  10636  resqrexlemex  10637  abs00ap  10674  absdiflt  10704  absdifle  10705  lenegsq  10707  cau3lem  10726  minmax  10840  xrmaxltsup  10866  xrminmax  10873  xrltmininf  10878  xrlemininf  10879  clim  10889  clim2  10891  clim0  10893  clim0c  10894  climi0  10897  climuni  10901  2clim  10909  climshftlemg  10910  climshft  10912  climabs0  10915  climcn1  10916  climcn2  10917  addcn2  10918  subcn2  10919  mulcn2  10920  iser3shft  10954  climcau  10955  serf0  10960  sumeq1  10963  sumeq2  10967  sumrbdc  10986  summodclem2  10990  summodc  10991  zsumdc  10992  isumshft  11098  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  tanaddaplem  11243  sin01bnd  11262  cos01bnd  11263  halfleoddlt  11386  gcddvds  11447  dvdssq  11512  lcmgcdlem  11551  lcmdvds  11553  isprm  11583  prmgt1  11605  isprm6  11618  pw2dvdslemn  11635  pw2dvdseu  11638  oddpwdclemxy  11639  oddpwdclemndvds  11641  oddpwdclemodd  11642  blfvalps  12313  elblps  12318  elbl  12319  elbl3ps  12322  elbl3  12323  blres  12362  comet  12427  bdbl  12431  metcnp2  12437  cnbl0  12456  cnblcld  12457  bl2ioo  12461  elcncf  12473  elcncf2  12474  cncfi  12478  rescncf  12481  mulc1cncf  12489  cncfco  12491  cncfmet  12492  cncfmptid  12496  addccncf  12498  cdivcncfap  12499  negcncf  12500  mulcncflem  12502  mulcncf  12503  limccl  12510  ellimc3ap  12511  limcdifap  12512  limcimolemlt  12513  limcresi  12515  cnplimcim  12516  limccnpcntop  12520  qdencn  12806  trilpolemlt1  12818