Theorem breq1d 4103

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 4096	. 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 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  eqnbrtrd  4111  eqbrtrd  4115  eqbrtrdi  4132  sbcbr2g  4151  pofun  4415  fmptco  5821  isorel  5959  isocnv  5962  isotr  5967  imbrov2fvoveq  6053  caovordig  6198  caovordg  6200  caovord  6204  xporderlem  6405  reldmtpos  6462  brtposg  6463  tpostpos  6473  tposoprab  6489  th3qlem2  6850  ensn1g  7014  fndmeng  7028  xpsneng  7049  xpcomco  7053  snnen2oprc  7089  tridc  7132  fimax2gtrilemstep  7133  unsnfidcel  7156  pm54.43  7455  pr1or2  7459  ccfunen  7543  ltsonq  7678  ltanqg  7680  ltmnqg  7681  archnqq  7697  prloc  7771  addnqprulem  7808  appdivnq  7843  mulnqpru  7849  mullocprlem  7850  1idpru  7871  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlem2  7940  cauappcvgprlemlim  7941  cauappcvgpr  7942  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemcl  7956  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  caucvgprlem1  7959  caucvgprlem2  7960  caucvgpr  7962  caucvgprprlemell  7965  caucvgprprlemelu  7966  caucvgprprlemcbv  7967  caucvgprprlemval  7968  caucvgprprlemnkltj  7969  caucvgprprlemnkeqj  7970  caucvgprprlemnbj  7973  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemopl  7977  caucvgprprlemlol  7978  caucvgprprlemopu  7979  caucvgprprlemloc  7983  caucvgprprlemclphr  7985  caucvgprprlemexbt  7986  caucvgprprlemexb  7987  caucvgprprlemaddq  7988  caucvgprprlem1  7989  caucvgprprlem2  7990  ltsosr  8044  ltasrg  8050  addgt0sr  8055  mulextsr1  8061  prsrlt  8067  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  caucvgsr  8082  ltpsrprg  8083  pitonnlem2  8127  pitonn  8128  recidpipr  8136  axpre-ltadd  8166  axpre-mulext  8168  nntopi  8174  axcaucvglemval  8177  axcaucvglemcau  8178  axcaucvglemres  8179  ltaddnegr  8664  ltsubadd  8671  lesubadd  8673  ltaddsub2  8676  leaddsub2  8678  ltaddpos  8691  lesub2  8696  ltsub2  8698  ltnegcon2  8703  lenegcon2  8706  addge01  8711  subge0  8714  suble0  8715  lesub0  8718  ltordlem  8721  apreap  8826  divap0b  8922  mulgt1  9102  ltmulgt11  9103  gt0div  9109  ge0div  9110  ltmuldiv  9113  ltmuldiv2  9114  lemuldiv2  9121  ltrec  9122  lerec2  9128  ltdiv23  9131  lediv23  9132  sup3exmid  9196  addltmul  9440  avglt1  9442  avgle1  9444  div4p1lem1div2  9457  ztri3or  9583  zlem1lt  9597  zgt0ge1  9599  qapne  9934  irrmulap  9943  divlt1lt  10020  divle1le  10021  xrltso  10092  xltnegi  10131  xltadd1  10172  xposdif  10178  xlesubadd  10179  xleaddadd  10183  nn0disj  10435  qavgle  10581  fldiv4lem1div2uz2  10629  frec2uzf1od  10731  iseqf1olemfvp  10835  seqf1oglem1  10844  exp3vallem  10865  expap0  10894  leexp2r  10918  sqap0  10931  nn0ltexp2  11034  nn0opthlem1d  11045  hashennnuni  11104  hashunlem  11130  zfz1isolemiso  11166  seq3coll  11169  swrdccatin2  11376  shftfvalg  11458  shftfibg  11460  shftfval  11461  shftfib  11463  shftfn  11464  2shfti  11471  shftidt2  11472  caucvgre  11621  cvg1nlemcau  11624  cvg1nlemres  11625  resqrexlemdecn  11652  resqrexlemoverl  11661  resqrexlemglsq  11662  resqrexlemsqa  11664  resqrexlemex  11665  abs00ap  11702  absdiflt  11732  absdifle  11733  lenegsq  11735  cau3lem  11754  minmax  11870  xrmaxltsup  11898  xrminmax  11905  xrltmininf  11910  xrlemininf  11911  clim  11921  clim2  11923  clim0  11925  clim0c  11926  climi0  11929  climuni  11933  2clim  11941  climshftlemg  11942  climshft  11944  climabs0  11947  climcn1  11948  climcn2  11949  addcn2  11950  subcn2  11951  mulcn2  11952  iser3shft  11986  climcau  11987  serf0  11992  sumeq1  11995  sumeq2  11999  sumrbdc  12020  summodclem2  12023  summodc  12024  zsumdc  12025  isumshft  12131  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodfap0  12186  prodfrecap  12187  prodfdivap  12188  ntrivcvgap  12189  ntrivcvgap0  12190  prodeq1f  12193  prodeq2w  12197  prodeq2  12198  prodrbdclem2  12214  prodmodclem2  12218  prodmodc  12219  zproddc  12220  fprodntrivap  12225  fprodap0  12262  fprodrec  12270  fproddivapf  12272  fprodap0f  12277  tanaddaplem  12379  sin01bnd  12398  cos01bnd  12399  halfleoddlt  12535  gcddvds  12614  dvdssq  12682  lcmgcdlem  12729  lcmdvds  12731  isprm  12761  prmgt1  12784  isprm5lem  12793  isprm6  12799  pw2dvdslemn  12817  pw2dvdseu  12820  oddpwdclemxy  12821  oddpwdclemndvds  12823  oddpwdclemodd  12824  odzdvds  12898  pclem0  12939  pclemub  12940  pclemdc  12941  pcprecl  12942  pcprendvds  12943  pcpremul  12946  pceulem  12947  pcval  12949  pcelnn  12974  pc2dvds  12983  pcadd  12993  pcadd2  12994  pcmpt  12996  prmpwdvds  13008  4sqlem17  13060  imasaddfnlemg  13477  znf1o  14747  znidomb  14754  mplsubgfilemm  14799  mplsubgfilemcl  14800  blfvalps  15196  elblps  15201  elbl  15202  elbl3ps  15205  elbl3  15206  blres  15245  comet  15310  bdbl  15314  xmetxp  15318  xmetxpbl  15319  metcnp2  15324  txmetcnp  15329  cnbl0  15345  cnblcld  15346  bl2ioo  15361  addcncntoplem  15372  divcnap  15376  mpomulcn  15377  elcncf  15384  elcncf2  15385  cncfi  15389  rescncf  15392  mulc1cncf  15400  cncfco  15402  cncfmet  15403  cncfmptid  15408  addccncf  15411  cdivcncfap  15415  negcncf  15416  mulcncflem  15418  mulcncf  15419  ivthinclemlm  15445  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemdisj  15451  ivthinclemloc  15452  ivthinc  15454  ivthreinc  15456  limccl  15470  ellimc3apf  15471  limcdifap  15473  limcmpted  15474  limcimolemlt  15475  limcresi  15477  cnplimcim  15478  limccnpcntop  15486  limccnp2lem  15487  limccoap  15489  dvcoapbr  15518  dveflem  15537  eflt  15586  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  logltb  15685  logge0b  15701  loggt0b  15702  pellexlem3  15793  lgslem2  15820  lgslem3  15821  lgsval  15823  lgsfcl2  15825  lgsfle1  15828  lgsle1  15834  lgsdirprm  15853  lgsne0  15857  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem2  15881  gausslemma2dlem3  15882  gausslemma2dlem4  15883  subupgr  16214  vtxdumgrfival  16239  qdencn  16755  trilpolemlt1  16773