Theorem breq1d 4028

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
breq1d	|- ( ph -> ( A R C <-> B R C ) )

Proof of Theorem breq1d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq1 4021	. 2 |- ( A = B -> ( A R C <-> B R C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A R C <-> B R C ) )

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  14342  elblps  14347  elbl  14348  elbl3ps  14351  elbl3  14352  blres  14391  comet  14456  bdbl  14460  xmetxp  14464  xmetxpbl  14465  metcnp2  14470  txmetcnp  14475  cnbl0  14491  cnblcld  14492  bl2ioo  14499  addcncntoplem  14508  divcnap  14512  elcncf  14517  elcncf2  14518  cncfi  14522  rescncf  14525  mulc1cncf  14533  cncfco  14535  cncfmet  14536  cncfmptid  14540  addccncf  14543  cdivcncfap  14544  negcncf  14545  mulcncflem  14547  mulcncf  14548  ivthinclemlm  14569  ivthinclemlopn  14571  ivthinclemlr  14572  ivthinclemuopn  14573  ivthinclemur  14574  ivthinclemdisj  14575  ivthinclemloc  14576  ivthinc  14578  limccl  14585  ellimc3apf  14586  limcdifap  14588  limcmpted  14589  limcimolemlt  14590  limcresi  14592  cnplimcim  14593  limccnpcntop  14601  limccnp2lem  14602  limccoap  14604  dvcoapbr  14628  dveflem  14644  eflt  14653  sincosq2sgn  14705  sincosq3sgn  14706  sincosq4sgn  14707  logltb  14752  logge0b  14768  loggt0b  14769  lgslem2  14860  lgslem3  14861  lgsval  14863  lgsfcl2  14865  lgsfle1  14868  lgsle1  14874  lgsdirprm  14893  lgsne0  14897  qdencn  15234  trilpolemlt1  15248