Theorem breq1d 4040

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 4033	. 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 4030

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 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  eqnbrtrd  4048  eqbrtrd  4052  eqbrtrdi  4069  sbcbr2g  4087  pofun  4344  fmptco  5725  isorel  5852  isocnv  5855  isotr  5860  imbrov2fvoveq  5944  caovordig  6086  caovordg  6088  caovord  6092  xporderlem  6286  reldmtpos  6308  brtposg  6309  tpostpos  6319  tposoprab  6335  th3qlem2  6694  ensn1g  6853  fndmeng  6866  xpsneng  6878  xpcomco  6882  snnen2oprc  6918  tridc  6957  fimax2gtrilemstep  6958  unsnfidcel  6979  pm54.43  7252  ccfunen  7326  ltsonq  7460  ltanqg  7462  ltmnqg  7463  archnqq  7479  prloc  7553  addnqprulem  7590  appdivnq  7625  mulnqpru  7631  mullocprlem  7632  1idpru  7653  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlem2  7722  cauappcvgprlemlim  7723  cauappcvgpr  7724  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnbj  7755  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlemexb  7769  caucvgprprlemaddq  7770  caucvgprprlem1  7771  caucvgprprlem2  7772  ltsosr  7826  ltasrg  7832  addgt0sr  7837  mulextsr1  7843  prsrlt  7849  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  caucvgsr  7864  ltpsrprg  7865  pitonnlem2  7909  pitonn  7910  recidpipr  7918  axpre-ltadd  7948  axpre-mulext  7950  nntopi  7956  axcaucvglemval  7959  axcaucvglemcau  7960  axcaucvglemres  7961  ltaddnegr  8446  ltsubadd  8453  lesubadd  8455  ltaddsub2  8458  leaddsub2  8460  ltaddpos  8473  lesub2  8478  ltsub2  8480  ltnegcon2  8485  lenegcon2  8488  addge01  8493  subge0  8496  suble0  8497  lesub0  8500  ltordlem  8503  apreap  8608  divap0b  8704  mulgt1  8884  ltmulgt11  8885  gt0div  8891  ge0div  8892  ltmuldiv  8895  ltmuldiv2  8896  lemuldiv2  8903  ltrec  8904  lerec2  8910  ltdiv23  8913  lediv23  8914  sup3exmid  8978  addltmul  9222  avglt1  9224  avgle1  9226  div4p1lem1div2  9239  ztri3or  9363  zlem1lt  9376  zgt0ge1  9378  qapne  9707  irrmulap  9716  divlt1lt  9793  divle1le  9794  xrltso  9865  xltnegi  9904  xltadd1  9945  xposdif  9951  xlesubadd  9952  xleaddadd  9956  nn0disj  10207  qavgle  10330  fldiv4lem1div2uz2  10378  frec2uzf1od  10480  iseqf1olemfvp  10584  seqf1oglem1  10593  exp3vallem  10614  expap0  10643  leexp2r  10667  sqap0  10680  nn0ltexp2  10783  nn0opthlem1d  10794  hashennnuni  10853  hashunlem  10878  zfz1isolemiso  10913  seq3coll  10916  shftfvalg  10965  shftfibg  10967  shftfval  10968  shftfib  10970  shftfn  10971  2shfti  10978  shftidt2  10979  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemdecn  11159  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  abs00ap  11209  absdiflt  11239  absdifle  11240  lenegsq  11242  cau3lem  11261  minmax  11376  xrmaxltsup  11404  xrminmax  11411  xrltmininf  11416  xrlemininf  11417  clim  11427  clim2  11429  clim0  11431  clim0c  11432  climi0  11435  climuni  11439  2clim  11447  climshftlemg  11448  climshft  11450  climabs0  11453  climcn1  11454  climcn2  11455  addcn2  11456  subcn2  11457  mulcn2  11458  iser3shft  11492  climcau  11493  serf0  11498  sumeq1  11501  sumeq2  11505  sumrbdc  11525  summodclem2  11528  summodc  11529  zsumdc  11530  isumshft  11636  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodfap0  11691  prodfrecap  11692  prodfdivap  11693  ntrivcvgap  11694  ntrivcvgap0  11695  prodeq1f  11698  prodeq2w  11702  prodeq2  11703  prodrbdclem2  11719  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodntrivap  11730  fprodap0  11767  fprodrec  11775  fproddivapf  11777  fprodap0f  11782  tanaddaplem  11884  sin01bnd  11903  cos01bnd  11904  halfleoddlt  12038  gcddvds  12103  dvdssq  12171  lcmgcdlem  12218  lcmdvds  12220  isprm  12250  prmgt1  12273  isprm5lem  12282  isprm6  12288  pw2dvdslemn  12306  pw2dvdseu  12309  oddpwdclemxy  12310  oddpwdclemndvds  12312  oddpwdclemodd  12313  odzdvds  12386  pclem0  12427  pclemub  12428  pclemdc  12429  pcprecl  12430  pcprendvds  12431  pcpremul  12434  pceulem  12435  pcval  12437  pcelnn  12462  pc2dvds  12471  pcadd  12481  pcadd2  12482  pcmpt  12484  prmpwdvds  12496  4sqlem17  12548  imasaddfnlemg  12900  znf1o  14150  znidomb  14157  blfvalps  14564  elblps  14569  elbl  14570  elbl3ps  14573  elbl3  14574  blres  14613  comet  14678  bdbl  14682  xmetxp  14686  xmetxpbl  14687  metcnp2  14692  txmetcnp  14697  cnbl0  14713  cnblcld  14714  bl2ioo  14729  addcncntoplem  14740  divcnap  14744  mpomulcn  14745  elcncf  14752  elcncf2  14753  cncfi  14757  rescncf  14760  mulc1cncf  14768  cncfco  14770  cncfmet  14771  cncfmptid  14776  addccncf  14779  cdivcncfap  14783  negcncf  14784  mulcncflem  14786  mulcncf  14787  ivthinclemlm  14813  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  ivthinc  14822  ivthreinc  14824  limccl  14838  ellimc3apf  14839  limcdifap  14841  limcmpted  14842  limcimolemlt  14843  limcresi  14845  cnplimcim  14846  limccnpcntop  14854  limccnp2lem  14855  limccoap  14857  dvcoapbr  14886  dveflem  14905  eflt  14951  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  logltb  15050  logge0b  15066  loggt0b  15067  lgslem2  15158  lgslem3  15159  lgsval  15161  lgsfcl2  15163  lgsfle1  15166  lgsle1  15172  lgsdirprm  15191  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  qdencn  15587  trilpolemlt1  15601