Theorem breq1d 4093

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 4086	. 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 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  eqnbrtrd  4101  eqbrtrd  4105  eqbrtrdi  4122  sbcbr2g  4141  pofun  4403  fmptco  5803  isorel  5938  isocnv  5941  isotr  5946  imbrov2fvoveq  6032  caovordig  6177  caovordg  6179  caovord  6183  xporderlem  6383  reldmtpos  6405  brtposg  6406  tpostpos  6416  tposoprab  6432  th3qlem2  6793  ensn1g  6957  fndmeng  6971  xpsneng  6989  xpcomco  6993  snnen2oprc  7029  tridc  7070  fimax2gtrilemstep  7071  unsnfidcel  7094  pm54.43  7374  pr1or2  7378  ccfunen  7461  ltsonq  7596  ltanqg  7598  ltmnqg  7599  archnqq  7615  prloc  7689  addnqprulem  7726  appdivnq  7761  mulnqpru  7767  mullocprlem  7768  1idpru  7789  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  caucvgprprlem1  7907  caucvgprprlem2  7908  ltsosr  7962  ltasrg  7968  addgt0sr  7973  mulextsr1  7979  prsrlt  7985  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  ltpsrprg  8001  pitonnlem2  8045  pitonn  8046  recidpipr  8054  axpre-ltadd  8084  axpre-mulext  8086  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  ltaddnegr  8583  ltsubadd  8590  lesubadd  8592  ltaddsub2  8595  leaddsub2  8597  ltaddpos  8610  lesub2  8615  ltsub2  8617  ltnegcon2  8622  lenegcon2  8625  addge01  8630  subge0  8633  suble0  8634  lesub0  8637  ltordlem  8640  apreap  8745  divap0b  8841  mulgt1  9021  ltmulgt11  9022  gt0div  9028  ge0div  9029  ltmuldiv  9032  ltmuldiv2  9033  lemuldiv2  9040  ltrec  9041  lerec2  9047  ltdiv23  9050  lediv23  9051  sup3exmid  9115  addltmul  9359  avglt1  9361  avgle1  9363  div4p1lem1div2  9376  ztri3or  9500  zlem1lt  9514  zgt0ge1  9516  qapne  9846  irrmulap  9855  divlt1lt  9932  divle1le  9933  xrltso  10004  xltnegi  10043  xltadd1  10084  xposdif  10090  xlesubadd  10091  xleaddadd  10095  nn0disj  10346  qavgle  10490  fldiv4lem1div2uz2  10538  frec2uzf1od  10640  iseqf1olemfvp  10744  seqf1oglem1  10753  exp3vallem  10774  expap0  10803  leexp2r  10827  sqap0  10840  nn0ltexp2  10943  nn0opthlem1d  10954  hashennnuni  11013  hashunlem  11038  zfz1isolemiso  11074  seq3coll  11077  swrdccatin2  11277  shftfvalg  11345  shftfibg  11347  shftfval  11348  shftfib  11350  shftfn  11351  2shfti  11358  shftidt2  11359  caucvgre  11508  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemdecn  11539  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemsqa  11551  resqrexlemex  11552  abs00ap  11589  absdiflt  11619  absdifle  11620  lenegsq  11622  cau3lem  11641  minmax  11757  xrmaxltsup  11785  xrminmax  11792  xrltmininf  11797  xrlemininf  11798  clim  11808  clim2  11810  clim0  11812  clim0c  11813  climi0  11816  climuni  11820  2clim  11828  climshftlemg  11829  climshft  11831  climabs0  11834  climcn1  11835  climcn2  11836  addcn2  11837  subcn2  11838  mulcn2  11839  iser3shft  11873  climcau  11874  serf0  11879  sumeq1  11882  sumeq2  11886  sumrbdc  11906  summodclem2  11909  summodc  11910  zsumdc  11911  isumshft  12017  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodfap0  12072  prodfrecap  12073  prodfdivap  12074  ntrivcvgap  12075  ntrivcvgap0  12076  prodeq1f  12079  prodeq2w  12083  prodeq2  12084  prodrbdclem2  12100  prodmodclem2  12104  prodmodc  12105  zproddc  12106  fprodntrivap  12111  fprodap0  12148  fprodrec  12156  fproddivapf  12158  fprodap0f  12163  tanaddaplem  12265  sin01bnd  12284  cos01bnd  12285  halfleoddlt  12421  gcddvds  12500  dvdssq  12568  lcmgcdlem  12615  lcmdvds  12617  isprm  12647  prmgt1  12670  isprm5lem  12679  isprm6  12685  pw2dvdslemn  12703  pw2dvdseu  12706  oddpwdclemxy  12707  oddpwdclemndvds  12709  oddpwdclemodd  12710  odzdvds  12784  pclem0  12825  pclemub  12826  pclemdc  12827  pcprecl  12828  pcprendvds  12829  pcpremul  12832  pceulem  12833  pcval  12835  pcelnn  12860  pc2dvds  12869  pcadd  12879  pcadd2  12880  pcmpt  12882  prmpwdvds  12894  4sqlem17  12946  imasaddfnlemg  13363  znf1o  14631  znidomb  14638  mplsubgfilemm  14678  mplsubgfilemcl  14679  blfvalps  15075  elblps  15080  elbl  15081  elbl3ps  15084  elbl3  15085  blres  15124  comet  15189  bdbl  15193  xmetxp  15197  xmetxpbl  15198  metcnp2  15203  txmetcnp  15208  cnbl0  15224  cnblcld  15225  bl2ioo  15240  addcncntoplem  15251  divcnap  15255  mpomulcn  15256  elcncf  15263  elcncf2  15264  cncfi  15268  rescncf  15271  mulc1cncf  15279  cncfco  15281  cncfmet  15282  cncfmptid  15287  addccncf  15290  cdivcncfap  15294  negcncf  15295  mulcncflem  15297  mulcncf  15298  ivthinclemlm  15324  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemdisj  15330  ivthinclemloc  15331  ivthinc  15333  ivthreinc  15335  limccl  15349  ellimc3apf  15350  limcdifap  15352  limcmpted  15353  limcimolemlt  15354  limcresi  15356  cnplimcim  15357  limccnpcntop  15365  limccnp2lem  15366  limccoap  15368  dvcoapbr  15397  dveflem  15416  eflt  15465  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  logltb  15564  logge0b  15580  loggt0b  15581  lgslem2  15696  lgslem3  15697  lgsval  15699  lgsfcl2  15701  lgsfle1  15704  lgsle1  15710  lgsdirprm  15729  lgsne0  15733  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem2  15757  gausslemma2dlem3  15758  gausslemma2dlem4  15759  vtxdumgrfival  16058  qdencn  16483  trilpolemlt1  16497