Theorem breq1d 4055

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 4048	. 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 1373   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  eqnbrtrd  4063  eqbrtrd  4067  eqbrtrdi  4084  sbcbr2g  4102  pofun  4360  fmptco  5748  isorel  5879  isocnv  5882  isotr  5887  imbrov2fvoveq  5971  caovordig  6114  caovordg  6116  caovord  6120  xporderlem  6319  reldmtpos  6341  brtposg  6342  tpostpos  6352  tposoprab  6368  th3qlem2  6727  ensn1g  6891  fndmeng  6904  xpsneng  6919  xpcomco  6923  snnen2oprc  6959  tridc  6998  fimax2gtrilemstep  6999  unsnfidcel  7020  pm54.43  7300  ccfunen  7378  ltsonq  7513  ltanqg  7515  ltmnqg  7516  archnqq  7532  prloc  7606  addnqprulem  7643  appdivnq  7678  mulnqpru  7684  mullocprlem  7685  1idpru  7706  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlem2  7775  cauappcvgprlemlim  7776  cauappcvgpr  7777  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkltj  7804  caucvgprprlemnkeqj  7805  caucvgprprlemnbj  7808  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  caucvgprprlemexb  7822  caucvgprprlemaddq  7823  caucvgprprlem1  7824  caucvgprprlem2  7825  ltsosr  7879  ltasrg  7885  addgt0sr  7890  mulextsr1  7896  prsrlt  7902  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  caucvgsr  7917  ltpsrprg  7918  pitonnlem2  7962  pitonn  7963  recidpipr  7971  axpre-ltadd  8001  axpre-mulext  8003  nntopi  8009  axcaucvglemval  8012  axcaucvglemcau  8013  axcaucvglemres  8014  ltaddnegr  8500  ltsubadd  8507  lesubadd  8509  ltaddsub2  8512  leaddsub2  8514  ltaddpos  8527  lesub2  8532  ltsub2  8534  ltnegcon2  8539  lenegcon2  8542  addge01  8547  subge0  8550  suble0  8551  lesub0  8554  ltordlem  8557  apreap  8662  divap0b  8758  mulgt1  8938  ltmulgt11  8939  gt0div  8945  ge0div  8946  ltmuldiv  8949  ltmuldiv2  8950  lemuldiv2  8957  ltrec  8958  lerec2  8964  ltdiv23  8967  lediv23  8968  sup3exmid  9032  addltmul  9276  avglt1  9278  avgle1  9280  div4p1lem1div2  9293  ztri3or  9417  zlem1lt  9431  zgt0ge1  9433  qapne  9762  irrmulap  9771  divlt1lt  9848  divle1le  9849  xrltso  9920  xltnegi  9959  xltadd1  10000  xposdif  10006  xlesubadd  10007  xleaddadd  10011  nn0disj  10262  qavgle  10403  fldiv4lem1div2uz2  10451  frec2uzf1od  10553  iseqf1olemfvp  10657  seqf1oglem1  10666  exp3vallem  10687  expap0  10716  leexp2r  10740  sqap0  10753  nn0ltexp2  10856  nn0opthlem1d  10867  hashennnuni  10926  hashunlem  10951  zfz1isolemiso  10986  seq3coll  10989  shftfvalg  11162  shftfibg  11164  shftfval  11165  shftfib  11167  shftfn  11168  2shfti  11175  shftidt2  11176  caucvgre  11325  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemdecn  11356  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  abs00ap  11406  absdiflt  11436  absdifle  11437  lenegsq  11439  cau3lem  11458  minmax  11574  xrmaxltsup  11602  xrminmax  11609  xrltmininf  11614  xrlemininf  11615  clim  11625  clim2  11627  clim0  11629  clim0c  11630  climi0  11633  climuni  11637  2clim  11645  climshftlemg  11646  climshft  11648  climabs0  11651  climcn1  11652  climcn2  11653  addcn2  11654  subcn2  11655  mulcn2  11656  iser3shft  11690  climcau  11691  serf0  11696  sumeq1  11699  sumeq2  11703  sumrbdc  11723  summodclem2  11726  summodc  11727  zsumdc  11728  isumshft  11834  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodfap0  11889  prodfrecap  11890  prodfdivap  11891  ntrivcvgap  11892  ntrivcvgap0  11893  prodeq1f  11896  prodeq2w  11900  prodeq2  11901  prodrbdclem2  11917  prodmodclem2  11921  prodmodc  11922  zproddc  11923  fprodntrivap  11928  fprodap0  11965  fprodrec  11973  fproddivapf  11975  fprodap0f  11980  tanaddaplem  12082  sin01bnd  12101  cos01bnd  12102  halfleoddlt  12238  gcddvds  12317  dvdssq  12385  lcmgcdlem  12432  lcmdvds  12434  isprm  12464  prmgt1  12487  isprm5lem  12496  isprm6  12502  pw2dvdslemn  12520  pw2dvdseu  12523  oddpwdclemxy  12524  oddpwdclemndvds  12526  oddpwdclemodd  12527  odzdvds  12601  pclem0  12642  pclemub  12643  pclemdc  12644  pcprecl  12645  pcprendvds  12646  pcpremul  12649  pceulem  12650  pcval  12652  pcelnn  12677  pc2dvds  12686  pcadd  12696  pcadd2  12697  pcmpt  12699  prmpwdvds  12711  4sqlem17  12763  imasaddfnlemg  13179  znf1o  14446  znidomb  14453  mplsubgfilemm  14493  mplsubgfilemcl  14494  blfvalps  14890  elblps  14895  elbl  14896  elbl3ps  14899  elbl3  14900  blres  14939  comet  15004  bdbl  15008  xmetxp  15012  xmetxpbl  15013  metcnp2  15018  txmetcnp  15023  cnbl0  15039  cnblcld  15040  bl2ioo  15055  addcncntoplem  15066  divcnap  15070  mpomulcn  15071  elcncf  15078  elcncf2  15079  cncfi  15083  rescncf  15086  mulc1cncf  15094  cncfco  15096  cncfmet  15097  cncfmptid  15102  addccncf  15105  cdivcncfap  15109  negcncf  15110  mulcncflem  15112  mulcncf  15113  ivthinclemlm  15139  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  ivthinc  15148  ivthreinc  15150  limccl  15164  ellimc3apf  15165  limcdifap  15167  limcmpted  15168  limcimolemlt  15169  limcresi  15171  cnplimcim  15172  limccnpcntop  15180  limccnp2lem  15181  limccoap  15183  dvcoapbr  15212  dveflem  15231  eflt  15280  sincosq2sgn  15332  sincosq3sgn  15333  sincosq4sgn  15334  logltb  15379  logge0b  15395  loggt0b  15396  lgslem2  15511  lgslem3  15512  lgsval  15514  lgsfcl2  15516  lgsfle1  15519  lgsle1  15525  lgsdirprm  15544  lgsne0  15548  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem2  15572  gausslemma2dlem3  15573  gausslemma2dlem4  15574  qdencn  16003  trilpolemlt1  16017