Theorem breq1d 4053

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   class class class wbr 4043

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  eqnbrtrd  4061  eqbrtrd  4065  eqbrtrdi  4082  sbcbr2g  4100  pofun  4358  fmptco  5745  isorel  5876  isocnv  5879  isotr  5884  imbrov2fvoveq  5968  caovordig  6111  caovordg  6113  caovord  6117  xporderlem  6316  reldmtpos  6338  brtposg  6339  tpostpos  6349  tposoprab  6365  th3qlem2  6724  ensn1g  6888  fndmeng  6901  xpsneng  6916  xpcomco  6920  snnen2oprc  6956  tridc  6995  fimax2gtrilemstep  6996  unsnfidcel  7017  pm54.43  7297  ccfunen  7375  ltsonq  7510  ltanqg  7512  ltmnqg  7513  archnqq  7529  prloc  7603  addnqprulem  7640  appdivnq  7675  mulnqpru  7681  mullocprlem  7682  1idpru  7703  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlem2  7772  cauappcvgprlemlim  7773  cauappcvgpr  7774  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnbj  7805  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlemexb  7819  caucvgprprlemaddq  7820  caucvgprprlem1  7821  caucvgprprlem2  7822  ltsosr  7876  ltasrg  7882  addgt0sr  7887  mulextsr1  7893  prsrlt  7899  caucvgsrlemgt1  7907  caucvgsrlemoffres  7912  caucvgsr  7914  ltpsrprg  7915  pitonnlem2  7959  pitonn  7960  recidpipr  7968  axpre-ltadd  7998  axpre-mulext  8000  nntopi  8006  axcaucvglemval  8009  axcaucvglemcau  8010  axcaucvglemres  8011  ltaddnegr  8497  ltsubadd  8504  lesubadd  8506  ltaddsub2  8509  leaddsub2  8511  ltaddpos  8524  lesub2  8529  ltsub2  8531  ltnegcon2  8536  lenegcon2  8539  addge01  8544  subge0  8547  suble0  8548  lesub0  8551  ltordlem  8554  apreap  8659  divap0b  8755  mulgt1  8935  ltmulgt11  8936  gt0div  8942  ge0div  8943  ltmuldiv  8946  ltmuldiv2  8947  lemuldiv2  8954  ltrec  8955  lerec2  8961  ltdiv23  8964  lediv23  8965  sup3exmid  9029  addltmul  9273  avglt1  9275  avgle1  9277  div4p1lem1div2  9290  ztri3or  9414  zlem1lt  9428  zgt0ge1  9430  qapne  9759  irrmulap  9768  divlt1lt  9845  divle1le  9846  xrltso  9917  xltnegi  9956  xltadd1  9997  xposdif  10003  xlesubadd  10004  xleaddadd  10008  nn0disj  10259  qavgle  10399  fldiv4lem1div2uz2  10447  frec2uzf1od  10549  iseqf1olemfvp  10653  seqf1oglem1  10662  exp3vallem  10683  expap0  10712  leexp2r  10736  sqap0  10749  nn0ltexp2  10852  nn0opthlem1d  10863  hashennnuni  10922  hashunlem  10947  zfz1isolemiso  10982  seq3coll  10985  shftfvalg  11100  shftfibg  11102  shftfval  11103  shftfib  11105  shftfn  11106  2shfti  11113  shftidt2  11114  caucvgre  11263  cvg1nlemcau  11266  cvg1nlemres  11267  resqrexlemdecn  11294  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemsqa  11306  resqrexlemex  11307  abs00ap  11344  absdiflt  11374  absdifle  11375  lenegsq  11377  cau3lem  11396  minmax  11512  xrmaxltsup  11540  xrminmax  11547  xrltmininf  11552  xrlemininf  11553  clim  11563  clim2  11565  clim0  11567  clim0c  11568  climi0  11571  climuni  11575  2clim  11583  climshftlemg  11584  climshft  11586  climabs0  11589  climcn1  11590  climcn2  11591  addcn2  11592  subcn2  11593  mulcn2  11594  iser3shft  11628  climcau  11629  serf0  11634  sumeq1  11637  sumeq2  11641  sumrbdc  11661  summodclem2  11664  summodc  11665  zsumdc  11666  isumshft  11772  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  prodfap0  11827  prodfrecap  11828  prodfdivap  11829  ntrivcvgap  11830  ntrivcvgap0  11831  prodeq1f  11834  prodeq2w  11838  prodeq2  11839  prodrbdclem2  11855  prodmodclem2  11859  prodmodc  11860  zproddc  11861  fprodntrivap  11866  fprodap0  11903  fprodrec  11911  fproddivapf  11913  fprodap0f  11918  tanaddaplem  12020  sin01bnd  12039  cos01bnd  12040  halfleoddlt  12176  gcddvds  12255  dvdssq  12323  lcmgcdlem  12370  lcmdvds  12372  isprm  12402  prmgt1  12425  isprm5lem  12434  isprm6  12440  pw2dvdslemn  12458  pw2dvdseu  12461  oddpwdclemxy  12462  oddpwdclemndvds  12464  oddpwdclemodd  12465  odzdvds  12539  pclem0  12580  pclemub  12581  pclemdc  12582  pcprecl  12583  pcprendvds  12584  pcpremul  12587  pceulem  12588  pcval  12590  pcelnn  12615  pc2dvds  12624  pcadd  12634  pcadd2  12635  pcmpt  12637  prmpwdvds  12649  4sqlem17  12701  imasaddfnlemg  13117  znf1o  14384  znidomb  14391  mplsubgfilemm  14431  mplsubgfilemcl  14432  blfvalps  14828  elblps  14833  elbl  14834  elbl3ps  14837  elbl3  14838  blres  14877  comet  14942  bdbl  14946  xmetxp  14950  xmetxpbl  14951  metcnp2  14956  txmetcnp  14961  cnbl0  14977  cnblcld  14978  bl2ioo  14993  addcncntoplem  15004  divcnap  15008  mpomulcn  15009  elcncf  15016  elcncf2  15017  cncfi  15021  rescncf  15024  mulc1cncf  15032  cncfco  15034  cncfmet  15035  cncfmptid  15040  addccncf  15043  cdivcncfap  15047  negcncf  15048  mulcncflem  15050  mulcncf  15051  ivthinclemlm  15077  ivthinclemlopn  15079  ivthinclemlr  15080  ivthinclemuopn  15081  ivthinclemur  15082  ivthinclemdisj  15083  ivthinclemloc  15084  ivthinc  15086  ivthreinc  15088  limccl  15102  ellimc3apf  15103  limcdifap  15105  limcmpted  15106  limcimolemlt  15107  limcresi  15109  cnplimcim  15110  limccnpcntop  15118  limccnp2lem  15119  limccoap  15121  dvcoapbr  15150  dveflem  15169  eflt  15218  sincosq2sgn  15270  sincosq3sgn  15271  sincosq4sgn  15272  logltb  15317  logge0b  15333  loggt0b  15334  lgslem2  15449  lgslem3  15450  lgsval  15452  lgsfcl2  15454  lgsfle1  15457  lgsle1  15463  lgsdirprm  15482  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  gausslemma2dlem2  15510  gausslemma2dlem3  15511  gausslemma2dlem4  15512  qdencn  15928  trilpolemlt1  15942