Theorem breq1d 4028

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019

This theorem is referenced by:  eqnbrtrd  4036  eqbrtrd  4040  eqbrtrdi  4057  sbcbr2g  4075  pofun  4330  fmptco  5703  isorel  5830  isocnv  5833  isotr  5838  imbrov2fvoveq  5921  caovordig  6062  caovordg  6064  caovord  6068  xporderlem  6256  reldmtpos  6278  brtposg  6279  tpostpos  6289  tposoprab  6305  th3qlem2  6664  ensn1g  6823  fndmeng  6836  xpsneng  6848  xpcomco  6852  snnen2oprc  6888  tridc  6927  fimax2gtrilemstep  6928  unsnfidcel  6949  pm54.43  7219  ccfunen  7293  ltsonq  7427  ltanqg  7429  ltmnqg  7430  archnqq  7446  prloc  7520  addnqprulem  7557  appdivnq  7592  mulnqpru  7598  mullocprlem  7599  1idpru  7620  cauappcvgprlemm  7674  cauappcvgprlemopl  7675  cauappcvgprlemlol  7676  cauappcvgprlemdisj  7680  cauappcvgprlemloc  7681  cauappcvgprlemladdfl  7684  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  cauappcvgprlem1  7688  cauappcvgprlem2  7689  cauappcvgprlemlim  7690  cauappcvgpr  7691  caucvgprlemnkj  7695  caucvgprlemnbj  7696  caucvgprlemm  7697  caucvgprlemopl  7698  caucvgprlemlol  7699  caucvgprlemdisj  7703  caucvgprlemloc  7704  caucvgprlemcl  7705  caucvgprlemladdfu  7706  caucvgprlemladdrl  7707  caucvgprlem1  7708  caucvgprlem2  7709  caucvgpr  7711  caucvgprprlemell  7714  caucvgprprlemelu  7715  caucvgprprlemcbv  7716  caucvgprprlemval  7717  caucvgprprlemnkltj  7718  caucvgprprlemnkeqj  7719  caucvgprprlemnbj  7722  caucvgprprlemml  7723  caucvgprprlemmu  7724  caucvgprprlemopl  7726  caucvgprprlemlol  7727  caucvgprprlemopu  7728  caucvgprprlemloc  7732  caucvgprprlemclphr  7734  caucvgprprlemexbt  7735  caucvgprprlemexb  7736  caucvgprprlemaddq  7737  caucvgprprlem1  7738  caucvgprprlem2  7739  ltsosr  7793  ltasrg  7799  addgt0sr  7804  mulextsr1  7810  prsrlt  7816  caucvgsrlemgt1  7824  caucvgsrlemoffres  7829  caucvgsr  7831  ltpsrprg  7832  pitonnlem2  7876  pitonn  7877  recidpipr  7885  axpre-ltadd  7915  axpre-mulext  7917  nntopi  7923  axcaucvglemval  7926  axcaucvglemcau  7927  axcaucvglemres  7928  ltaddnegr  8412  ltsubadd  8419  lesubadd  8421  ltaddsub2  8424  leaddsub2  8426  ltaddpos  8439  lesub2  8444  ltsub2  8446  ltnegcon2  8451  lenegcon2  8454  addge01  8459  subge0  8462  suble0  8463  lesub0  8466  ltordlem  8469  apreap  8574  divap0b  8670  mulgt1  8850  ltmulgt11  8851  gt0div  8857  ge0div  8858  ltmuldiv  8861  ltmuldiv2  8862  lemuldiv2  8869  ltrec  8870  lerec2  8876  ltdiv23  8879  lediv23  8880  sup3exmid  8944  addltmul  9185  avglt1  9187  avgle1  9189  div4p1lem1div2  9202  ztri3or  9326  zlem1lt  9339  zgt0ge1  9341  qapne  9669  divlt1lt  9754  divle1le  9755  xrltso  9826  xltnegi  9865  xltadd1  9906  xposdif  9912  xlesubadd  9913  xleaddadd  9917  nn0disj  10168  qavgle  10289  frec2uzf1od  10437  iseqf1olemfvp  10528  exp3vallem  10552  expap0  10581  leexp2r  10605  sqap0  10618  nn0ltexp2  10721  nn0opthlem1d  10732  hashennnuni  10791  hashunlem  10816  zfz1isolemiso  10851  seq3coll  10854  shftfvalg  10859  shftfibg  10861  shftfval  10862  shftfib  10864  shftfn  10865  2shfti  10872  shftidt2  10873  caucvgre  11022  cvg1nlemcau  11025  cvg1nlemres  11026  resqrexlemdecn  11053  resqrexlemoverl  11062  resqrexlemglsq  11063  resqrexlemsqa  11065  resqrexlemex  11066  abs00ap  11103  absdiflt  11133  absdifle  11134  lenegsq  11136  cau3lem  11155  minmax  11270  xrmaxltsup  11298  xrminmax  11305  xrltmininf  11310  xrlemininf  11311  clim  11321  clim2  11323  clim0  11325  clim0c  11326  climi0  11329  climuni  11333  2clim  11341  climshftlemg  11342  climshft  11344  climabs0  11347  climcn1  11348  climcn2  11349  addcn2  11350  subcn2  11351  mulcn2  11352  iser3shft  11386  climcau  11387  serf0  11392  sumeq1  11395  sumeq2  11399  sumrbdc  11419  summodclem2  11422  summodc  11423  zsumdc  11424  isumshft  11530  mertenslemi1  11575  mertenslem2  11576  mertensabs  11577  prodfap0  11585  prodfrecap  11586  prodfdivap  11587  ntrivcvgap  11588  ntrivcvgap0  11589  prodeq1f  11592  prodeq2w  11596  prodeq2  11597  prodrbdclem2  11613  prodmodclem2  11617  prodmodc  11618  zproddc  11619  fprodntrivap  11624  fprodap0  11661  fprodrec  11669  fproddivapf  11671  fprodap0f  11676  tanaddaplem  11778  sin01bnd  11797  cos01bnd  11798  halfleoddlt  11931  gcddvds  11996  dvdssq  12064  lcmgcdlem  12109  lcmdvds  12111  isprm  12141  prmgt1  12164  isprm5lem  12173  isprm6  12179  pw2dvdslemn  12197  pw2dvdseu  12200  oddpwdclemxy  12201  oddpwdclemndvds  12203  oddpwdclemodd  12204  odzdvds  12277  pclem0  12318  pclemub  12319  pclemdc  12320  pcprecl  12321  pcprendvds  12322  pcpremul  12325  pceulem  12326  pcval  12328  pcelnn  12353  pc2dvds  12362  pcadd  12372  pcadd2  12373  pcmpt  12375  prmpwdvds  12387  4sqlem17  12439  imasaddfnlemg  12791  blfvalps  14345  elblps  14350  elbl  14351  elbl3ps  14354  elbl3  14355  blres  14394  comet  14459  bdbl  14463  xmetxp  14467  xmetxpbl  14468  metcnp2  14473  txmetcnp  14478  cnbl0  14494  cnblcld  14495  bl2ioo  14502  addcncntoplem  14511  divcnap  14515  elcncf  14520  elcncf2  14521  cncfi  14525  rescncf  14528  mulc1cncf  14536  cncfco  14538  cncfmet  14539  cncfmptid  14543  addccncf  14546  cdivcncfap  14547  negcncf  14548  mulcncflem  14550  mulcncf  14551  ivthinclemlm  14572  ivthinclemlopn  14574  ivthinclemlr  14575  ivthinclemuopn  14576  ivthinclemur  14577  ivthinclemdisj  14578  ivthinclemloc  14579  ivthinc  14581  limccl  14588  ellimc3apf  14589  limcdifap  14591  limcmpted  14592  limcimolemlt  14593  limcresi  14595  cnplimcim  14596  limccnpcntop  14604  limccnp2lem  14605  limccoap  14607  dvcoapbr  14631  dveflem  14647  eflt  14656  sincosq2sgn  14708  sincosq3sgn  14709  sincosq4sgn  14710  logltb  14755  logge0b  14771  loggt0b  14772  lgslem2  14863  lgslem3  14864  lgsval  14866  lgsfcl2  14868  lgsfle1  14871  lgsle1  14877  lgsdirprm  14896  lgsne0  14900  qdencn  15237  trilpolemlt1  15251