Theorem breq1d 4044

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4034

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  eqnbrtrd  4052  eqbrtrd  4056  eqbrtrdi  4073  sbcbr2g  4091  pofun  4348  fmptco  5731  isorel  5858  isocnv  5861  isotr  5866  imbrov2fvoveq  5950  caovordig  6093  caovordg  6095  caovord  6099  xporderlem  6298  reldmtpos  6320  brtposg  6321  tpostpos  6331  tposoprab  6347  th3qlem2  6706  ensn1g  6865  fndmeng  6878  xpsneng  6890  xpcomco  6894  snnen2oprc  6930  tridc  6969  fimax2gtrilemstep  6970  unsnfidcel  6991  pm54.43  7271  ccfunen  7349  ltsonq  7484  ltanqg  7486  ltmnqg  7487  archnqq  7503  prloc  7577  addnqprulem  7614  appdivnq  7649  mulnqpru  7655  mullocprlem  7656  1idpru  7677  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlem2  7746  cauappcvgprlemlim  7747  cauappcvgpr  7748  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemclphr  7791  caucvgprprlemexbt  7792  caucvgprprlemexb  7793  caucvgprprlemaddq  7794  caucvgprprlem1  7795  caucvgprprlem2  7796  ltsosr  7850  ltasrg  7856  addgt0sr  7861  mulextsr1  7867  prsrlt  7873  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  caucvgsr  7888  ltpsrprg  7889  pitonnlem2  7933  pitonn  7934  recidpipr  7942  axpre-ltadd  7972  axpre-mulext  7974  nntopi  7980  axcaucvglemval  7983  axcaucvglemcau  7984  axcaucvglemres  7985  ltaddnegr  8471  ltsubadd  8478  lesubadd  8480  ltaddsub2  8483  leaddsub2  8485  ltaddpos  8498  lesub2  8503  ltsub2  8505  ltnegcon2  8510  lenegcon2  8513  addge01  8518  subge0  8521  suble0  8522  lesub0  8525  ltordlem  8528  apreap  8633  divap0b  8729  mulgt1  8909  ltmulgt11  8910  gt0div  8916  ge0div  8917  ltmuldiv  8920  ltmuldiv2  8921  lemuldiv2  8928  ltrec  8929  lerec2  8935  ltdiv23  8938  lediv23  8939  sup3exmid  9003  addltmul  9247  avglt1  9249  avgle1  9251  div4p1lem1div2  9264  ztri3or  9388  zlem1lt  9401  zgt0ge1  9403  qapne  9732  irrmulap  9741  divlt1lt  9818  divle1le  9819  xrltso  9890  xltnegi  9929  xltadd1  9970  xposdif  9976  xlesubadd  9977  xleaddadd  9981  nn0disj  10232  qavgle  10367  fldiv4lem1div2uz2  10415  frec2uzf1od  10517  iseqf1olemfvp  10621  seqf1oglem1  10630  exp3vallem  10651  expap0  10680  leexp2r  10704  sqap0  10717  nn0ltexp2  10820  nn0opthlem1d  10831  hashennnuni  10890  hashunlem  10915  zfz1isolemiso  10950  seq3coll  10953  shftfvalg  11002  shftfibg  11004  shftfval  11005  shftfib  11007  shftfn  11008  2shfti  11015  shftidt2  11016  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemdecn  11196  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemsqa  11208  resqrexlemex  11209  abs00ap  11246  absdiflt  11276  absdifle  11277  lenegsq  11279  cau3lem  11298  minmax  11414  xrmaxltsup  11442  xrminmax  11449  xrltmininf  11454  xrlemininf  11455  clim  11465  clim2  11467  clim0  11469  clim0c  11470  climi0  11473  climuni  11477  2clim  11485  climshftlemg  11486  climshft  11488  climabs0  11491  climcn1  11492  climcn2  11493  addcn2  11494  subcn2  11495  mulcn2  11496  iser3shft  11530  climcau  11531  serf0  11536  sumeq1  11539  sumeq2  11543  sumrbdc  11563  summodclem2  11566  summodc  11567  zsumdc  11568  isumshft  11674  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodfap0  11729  prodfrecap  11730  prodfdivap  11731  ntrivcvgap  11732  ntrivcvgap0  11733  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  prodrbdclem2  11757  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodntrivap  11768  fprodap0  11805  fprodrec  11813  fproddivapf  11815  fprodap0f  11820  tanaddaplem  11922  sin01bnd  11941  cos01bnd  11942  halfleoddlt  12078  gcddvds  12157  dvdssq  12225  lcmgcdlem  12272  lcmdvds  12274  isprm  12304  prmgt1  12327  isprm5lem  12336  isprm6  12342  pw2dvdslemn  12360  pw2dvdseu  12363  oddpwdclemxy  12364  oddpwdclemndvds  12366  oddpwdclemodd  12367  odzdvds  12441  pclem0  12482  pclemub  12483  pclemdc  12484  pcprecl  12485  pcprendvds  12486  pcpremul  12489  pceulem  12490  pcval  12492  pcelnn  12517  pc2dvds  12526  pcadd  12536  pcadd2  12537  pcmpt  12539  prmpwdvds  12551  4sqlem17  12603  imasaddfnlemg  13018  znf1o  14285  znidomb  14292  mplsubgfilemm  14332  mplsubgfilemcl  14333  blfvalps  14729  elblps  14734  elbl  14735  elbl3ps  14738  elbl3  14739  blres  14778  comet  14843  bdbl  14847  xmetxp  14851  xmetxpbl  14852  metcnp2  14857  txmetcnp  14862  cnbl0  14878  cnblcld  14879  bl2ioo  14894  addcncntoplem  14905  divcnap  14909  mpomulcn  14910  elcncf  14917  elcncf2  14918  cncfi  14922  rescncf  14925  mulc1cncf  14933  cncfco  14935  cncfmet  14936  cncfmptid  14941  addccncf  14944  cdivcncfap  14948  negcncf  14949  mulcncflem  14951  mulcncf  14952  ivthinclemlm  14978  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemdisj  14984  ivthinclemloc  14985  ivthinc  14987  ivthreinc  14989  limccl  15003  ellimc3apf  15004  limcdifap  15006  limcmpted  15007  limcimolemlt  15008  limcresi  15010  cnplimcim  15011  limccnpcntop  15019  limccnp2lem  15020  limccoap  15022  dvcoapbr  15051  dveflem  15070  eflt  15119  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  logltb  15218  logge0b  15234  loggt0b  15235  lgslem2  15350  lgslem3  15351  lgsval  15353  lgsfcl2  15355  lgsfle1  15358  lgsle1  15364  lgsdirprm  15383  lgsne0  15387  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem2  15411  gausslemma2dlem3  15412  gausslemma2dlem4  15413  qdencn  15784  trilpolemlt1  15798