Theorem breq1d 4124

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  eqnbrtrd  4132  eqbrtrd  4136  eqbrtrdi  4153  sbcbr2g  4172  pofun  4438  fmptco  5848  isorel  5987  isocnv  5990  isotr  5995  imbrov2fvoveq  6083  caovordig  6228  caovordg  6230  caovord  6234  xporderlem  6440  reldmtpos  6497  brtposg  6498  tpostpos  6508  tposoprab  6524  th3qlem2  6885  ensn1g  7050  fndmeng  7064  xpsneng  7086  xpcomco  7090  snnen2oprc  7127  tridc  7170  fimax2gtrilemstep  7171  unsnfidcel  7194  pm54.43  7500  pr1or2  7504  ccfunen  7594  ltsonq  7729  ltanqg  7731  ltmnqg  7732  archnqq  7748  prloc  7822  addnqprulem  7859  appdivnq  7894  mulnqpru  7900  mullocprlem  7901  1idpru  7922  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlemexb  8038  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  ltsosr  8095  ltasrg  8101  addgt0sr  8106  mulextsr1  8112  prsrlt  8118  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  ltpsrprg  8134  pitonnlem2  8178  pitonn  8179  recidpipr  8187  axpre-ltadd  8217  axpre-mulext  8219  nntopi  8225  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  ltaddnegr  8716  ltsubadd  8723  lesubadd  8725  ltaddsub2  8728  leaddsub2  8730  ltaddpos  8743  lesub2  8748  ltsub2  8750  ltnegcon2  8755  lenegcon2  8758  addge01  8763  subge0  8766  suble0  8767  lesub0  8770  ltordlem  8773  apreap  8878  divap0b  8974  mulgt1  9154  ltmulgt11  9155  gt0div  9161  ge0div  9162  ltmuldiv  9165  ltmuldiv2  9166  lemuldiv2  9173  ltrec  9174  lerec2  9180  ltdiv23  9183  lediv23  9184  sup3exmid  9248  addltmul  9492  avglt1  9494  avgle1  9496  div4p1lem1div2  9509  ztri3or  9637  zlem1lt  9651  zgt0ge1  9653  qapne  9989  irrmulap  9998  divlt1lt  10075  divle1le  10076  xrltso  10148  xltnegi  10187  xltadd1  10228  xposdif  10234  xlesubadd  10235  xleaddadd  10239  nn0disj  10494  qavgle  10642  fldiv4lem1div2uz2  10690  frec2uzf1od  10792  iseqf1olemfvp  10896  seqf1oglem1  10905  exp3vallem  10926  expap0  10955  leexp2r  10979  sqap0  10992  nn0ltexp2  11096  nn0opthlem1d  11107  hashennnuni  11167  hashunlem  11193  zfz1isolemiso  11236  seq3coll  11239  swrdccatin2  11446  shftfvalg  11528  shftfibg  11530  shftfval  11531  shftfib  11533  shftfn  11534  2shfti  11541  shftidt2  11542  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemdecn  11722  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  abs00ap  11772  absdiflt  11802  absdifle  11803  lenegsq  11805  cau3lem  11824  minmax  11940  xrmaxltsup  11968  xrminmax  11975  xrltmininf  11980  xrlemininf  11981  clim  11991  clim2  11993  clim0  11995  clim0c  11996  climi0  11999  climuni  12003  2clim  12011  climshftlemg  12012  climshft  12014  climabs0  12017  climcn1  12018  climcn2  12019  addcn2  12020  subcn2  12021  mulcn2  12022  iser3shft  12056  climcau  12057  serf0  12062  sumeq1  12065  sumeq2  12069  sumrbdc  12090  summodclem2  12093  summodc  12094  zsumdc  12095  isumshft  12201  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodfap0  12256  prodfrecap  12257  prodfdivap  12258  ntrivcvgap  12259  ntrivcvgap0  12260  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  prodrbdclem2  12284  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodntrivap  12295  fprodap0  12332  fprodrec  12340  fproddivapf  12342  fprodap0f  12347  tanaddaplem  12449  sin01bnd  12468  cos01bnd  12469  halfleoddlt  12605  gcddvds  12684  dvdssq  12752  lcmgcdlem  12799  lcmdvds  12801  isprm  12831  prmgt1  12854  isprm5lem  12863  isprm6  12869  pw2dvdslemn  12887  pw2dvdseu  12890  oddpwdclemxy  12891  oddpwdclemndvds  12893  oddpwdclemodd  12894  odzdvds  12968  pclem0  13009  pclemub  13010  pclemdc  13011  pcprecl  13012  pcprendvds  13013  pcpremul  13016  pceulem  13017  pcval  13019  pcelnn  13044  pc2dvds  13053  pcadd  13063  pcadd2  13064  pcmpt  13066  prmpwdvds  13078  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemic  13194  ballotfilemsv  13197  ballotfilemrc  13218  imasaddfnlemg  13578  znf1o  14925  znidomb  14932  mplsubgfilemm  14979  mplsubgfilemcl  14980  blfvalps  15376  elblps  15381  elbl  15382  elbl3ps  15385  elbl3  15386  blres  15425  comet  15490  bdbl  15494  xmetxp  15498  xmetxpbl  15499  metcnp2  15504  txmetcnp  15509  cnbl0  15525  cnblcld  15526  bl2ioo  15541  addcncntoplem  15552  divcnap  15556  mpomulcn  15557  elcncf  15564  elcncf2  15565  cncfi  15569  rescncf  15572  mulc1cncf  15580  cncfco  15582  cncfmet  15583  cncfmptid  15588  addccncf  15591  cdivcncfap  15595  negcncf  15596  mulcncflem  15598  mulcncf  15599  ivthinclemlm  15625  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  ivthinc  15634  ivthreinc  15636  limccl  15650  ellimc3apf  15651  limcdifap  15653  limcmpted  15654  limcimolemlt  15655  limcresi  15657  cnplimcim  15658  limccnpcntop  15666  limccnp2lem  15667  limccoap  15669  dvcoapbr  15698  dveflem  15717  eflt  15766  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  logltb  15865  logge0b  15881  loggt0b  15882  pellexlem3  15973  lgslem2  16000  lgslem3  16001  lgsval  16003  lgsfcl2  16005  lgsfle1  16008  lgsle1  16014  lgsdirprm  16033  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem2  16061  gausslemma2dlem3  16062  gausslemma2dlem4  16063  subupgr  16394  vtxdumgrfival  16419  qdencn  16933  trilpolemlt1  16951