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  5801  isorel  5932  isocnv  5935  isotr  5940  imbrov2fvoveq  6026  caovordig  6171  caovordg  6173  caovord  6177  xporderlem  6377  reldmtpos  6399  brtposg  6400  tpostpos  6410  tposoprab  6426  th3qlem2  6785  ensn1g  6949  fndmeng  6963  xpsneng  6981  xpcomco  6985  snnen2oprc  7021  tridc  7061  fimax2gtrilemstep  7062  unsnfidcel  7083  pm54.43  7363  pr1or2  7367  ccfunen  7450  ltsonq  7585  ltanqg  7587  ltmnqg  7588  archnqq  7604  prloc  7678  addnqprulem  7715  appdivnq  7750  mulnqpru  7756  mullocprlem  7757  1idpru  7778  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdfl  7842  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlem2  7847  cauappcvgprlemlim  7848  cauappcvgpr  7849  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnkltj  7876  caucvgprprlemnkeqj  7877  caucvgprprlemnbj  7880  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlemclphr  7892  caucvgprprlemexbt  7893  caucvgprprlemexb  7894  caucvgprprlemaddq  7895  caucvgprprlem1  7896  caucvgprprlem2  7897  ltsosr  7951  ltasrg  7957  addgt0sr  7962  mulextsr1  7968  prsrlt  7974  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  caucvgsr  7989  ltpsrprg  7990  pitonnlem2  8034  pitonn  8035  recidpipr  8043  axpre-ltadd  8073  axpre-mulext  8075  nntopi  8081  axcaucvglemval  8084  axcaucvglemcau  8085  axcaucvglemres  8086  ltaddnegr  8572  ltsubadd  8579  lesubadd  8581  ltaddsub2  8584  leaddsub2  8586  ltaddpos  8599  lesub2  8604  ltsub2  8606  ltnegcon2  8611  lenegcon2  8614  addge01  8619  subge0  8622  suble0  8623  lesub0  8626  ltordlem  8629  apreap  8734  divap0b  8830  mulgt1  9010  ltmulgt11  9011  gt0div  9017  ge0div  9018  ltmuldiv  9021  ltmuldiv2  9022  lemuldiv2  9029  ltrec  9030  lerec2  9036  ltdiv23  9039  lediv23  9040  sup3exmid  9104  addltmul  9348  avglt1  9350  avgle1  9352  div4p1lem1div2  9365  ztri3or  9489  zlem1lt  9503  zgt0ge1  9505  qapne  9834  irrmulap  9843  divlt1lt  9920  divle1le  9921  xrltso  9992  xltnegi  10031  xltadd1  10072  xposdif  10078  xlesubadd  10079  xleaddadd  10083  nn0disj  10334  qavgle  10478  fldiv4lem1div2uz2  10526  frec2uzf1od  10628  iseqf1olemfvp  10732  seqf1oglem1  10741  exp3vallem  10762  expap0  10791  leexp2r  10815  sqap0  10828  nn0ltexp2  10931  nn0opthlem1d  10942  hashennnuni  11001  hashunlem  11026  zfz1isolemiso  11061  seq3coll  11064  swrdccatin2  11261  shftfvalg  11329  shftfibg  11331  shftfval  11332  shftfib  11334  shftfn  11335  2shfti  11342  shftidt2  11343  caucvgre  11492  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemdecn  11523  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  abs00ap  11573  absdiflt  11603  absdifle  11604  lenegsq  11606  cau3lem  11625  minmax  11741  xrmaxltsup  11769  xrminmax  11776  xrltmininf  11781  xrlemininf  11782  clim  11792  clim2  11794  clim0  11796  clim0c  11797  climi0  11800  climuni  11804  2clim  11812  climshftlemg  11813  climshft  11815  climabs0  11818  climcn1  11819  climcn2  11820  addcn2  11821  subcn2  11822  mulcn2  11823  iser3shft  11857  climcau  11858  serf0  11863  sumeq1  11866  sumeq2  11870  sumrbdc  11890  summodclem2  11893  summodc  11894  zsumdc  11895  isumshft  12001  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodfap0  12056  prodfrecap  12057  prodfdivap  12058  ntrivcvgap  12059  ntrivcvgap0  12060  prodeq1f  12063  prodeq2w  12067  prodeq2  12068  prodrbdclem2  12084  prodmodclem2  12088  prodmodc  12089  zproddc  12090  fprodntrivap  12095  fprodap0  12132  fprodrec  12140  fproddivapf  12142  fprodap0f  12147  tanaddaplem  12249  sin01bnd  12268  cos01bnd  12269  halfleoddlt  12405  gcddvds  12484  dvdssq  12552  lcmgcdlem  12599  lcmdvds  12601  isprm  12631  prmgt1  12654  isprm5lem  12663  isprm6  12669  pw2dvdslemn  12687  pw2dvdseu  12690  oddpwdclemxy  12691  oddpwdclemndvds  12693  oddpwdclemodd  12694  odzdvds  12768  pclem0  12809  pclemub  12810  pclemdc  12811  pcprecl  12812  pcprendvds  12813  pcpremul  12816  pceulem  12817  pcval  12819  pcelnn  12844  pc2dvds  12853  pcadd  12863  pcadd2  12864  pcmpt  12866  prmpwdvds  12878  4sqlem17  12930  imasaddfnlemg  13347  znf1o  14615  znidomb  14622  mplsubgfilemm  14662  mplsubgfilemcl  14663  blfvalps  15059  elblps  15064  elbl  15065  elbl3ps  15068  elbl3  15069  blres  15108  comet  15173  bdbl  15177  xmetxp  15181  xmetxpbl  15182  metcnp2  15187  txmetcnp  15192  cnbl0  15208  cnblcld  15209  bl2ioo  15224  addcncntoplem  15235  divcnap  15239  mpomulcn  15240  elcncf  15247  elcncf2  15248  cncfi  15252  rescncf  15255  mulc1cncf  15263  cncfco  15265  cncfmet  15266  cncfmptid  15271  addccncf  15274  cdivcncfap  15278  negcncf  15279  mulcncflem  15281  mulcncf  15282  ivthinclemlm  15308  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemdisj  15314  ivthinclemloc  15315  ivthinc  15317  ivthreinc  15319  limccl  15333  ellimc3apf  15334  limcdifap  15336  limcmpted  15337  limcimolemlt  15338  limcresi  15340  cnplimcim  15341  limccnpcntop  15349  limccnp2lem  15350  limccoap  15352  dvcoapbr  15381  dveflem  15400  eflt  15449  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  logltb  15548  logge0b  15564  loggt0b  15565  lgslem2  15680  lgslem3  15681  lgsval  15683  lgsfcl2  15685  lgsfle1  15688  lgsle1  15694  lgsdirprm  15713  lgsne0  15717  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem2  15741  gausslemma2dlem3  15742  gausslemma2dlem4  15743  qdencn  16395  trilpolemlt1  16409