Theorem breq1d 3947

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 3940	. 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 104   = wceq 1332   class class class wbr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938

This theorem is referenced by:  eqbrtrd  3958  eqbrtrdi  3975  sbcbr2g  3993  pofun  4242  fmptco  5594  isorel  5717  isocnv  5720  isotr  5725  imbrov2fvoveq  5807  caovordig  5944  caovordg  5946  caovord  5950  xporderlem  6136  reldmtpos  6158  brtposg  6159  tpostpos  6169  tposoprab  6185  th3qlem2  6540  ensn1g  6699  fndmeng  6712  xpsneng  6724  xpcomco  6728  snnen2oprc  6762  tridc  6801  fimax2gtrilemstep  6802  unsnfidcel  6817  pm54.43  7063  ccfunen  7096  ltsonq  7230  ltanqg  7232  ltmnqg  7233  archnqq  7249  prloc  7323  addnqprulem  7360  appdivnq  7395  mulnqpru  7401  mullocprlem  7402  1idpru  7423  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlem2  7492  cauappcvgprlemlim  7493  cauappcvgpr  7494  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprlem2  7512  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnbj  7525  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlemexb  7539  caucvgprprlemaddq  7540  caucvgprprlem1  7541  caucvgprprlem2  7542  ltsosr  7596  ltasrg  7602  addgt0sr  7607  mulextsr1  7613  prsrlt  7619  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  caucvgsr  7634  ltpsrprg  7635  pitonnlem2  7679  pitonn  7680  recidpipr  7688  axpre-ltadd  7718  axpre-mulext  7720  nntopi  7726  axcaucvglemval  7729  axcaucvglemcau  7730  axcaucvglemres  7731  ltaddnegr  8211  ltsubadd  8218  lesubadd  8220  ltaddsub2  8223  leaddsub2  8225  ltaddpos  8238  lesub2  8243  ltsub2  8245  ltnegcon2  8250  lenegcon2  8253  addge01  8258  subge0  8261  suble0  8262  lesub0  8265  ltordlem  8268  apreap  8373  divap0b  8467  mulgt1  8645  ltmulgt11  8646  gt0div  8652  ge0div  8653  ltmuldiv  8656  ltmuldiv2  8657  lemuldiv2  8664  ltrec  8665  lerec2  8671  ltdiv23  8674  lediv23  8675  sup3exmid  8739  addltmul  8980  avglt1  8982  avgle1  8984  div4p1lem1div2  8997  ztri3or  9121  zlem1lt  9134  zgt0ge1  9136  qapne  9458  divlt1lt  9541  divle1le  9542  xrltso  9612  xltnegi  9648  xltadd1  9689  xposdif  9695  xlesubadd  9696  xleaddadd  9700  nn0disj  9946  qavgle  10067  frec2uzf1od  10210  iseqf1olemfvp  10301  exp3vallem  10325  expap0  10354  leexp2r  10378  sqap0  10390  nn0opthlem1d  10498  hashennnuni  10557  hashunlem  10582  zfz1isolemiso  10614  seq3coll  10617  shftfvalg  10622  shftfibg  10624  shftfval  10625  shftfib  10627  shftfn  10628  2shfti  10635  shftidt2  10636  caucvgre  10785  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemdecn  10816  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  abs00ap  10866  absdiflt  10896  absdifle  10897  lenegsq  10899  cau3lem  10918  minmax  11033  xrmaxltsup  11059  xrminmax  11066  xrltmininf  11071  xrlemininf  11072  clim  11082  clim2  11084  clim0  11086  clim0c  11087  climi0  11090  climuni  11094  2clim  11102  climshftlemg  11103  climshft  11105  climabs0  11108  climcn1  11109  climcn2  11110  addcn2  11111  subcn2  11112  mulcn2  11113  iser3shft  11147  climcau  11148  serf0  11153  sumeq1  11156  sumeq2  11160  sumrbdc  11180  summodclem2  11183  summodc  11184  zsumdc  11185  isumshft  11291  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodfap0  11346  prodfrecap  11347  prodfdivap  11348  ntrivcvgap  11349  ntrivcvgap0  11350  prodeq1f  11353  prodeq2w  11357  prodeq2  11358  prodrbdclem2  11374  prodmodclem2  11378  prodmodc  11379  zproddc  11380  tanaddaplem  11481  sin01bnd  11500  cos01bnd  11501  halfleoddlt  11627  gcddvds  11688  dvdssq  11755  lcmgcdlem  11794  lcmdvds  11796  isprm  11826  prmgt1  11848  isprm6  11861  pw2dvdslemn  11879  pw2dvdseu  11882  oddpwdclemxy  11883  oddpwdclemndvds  11885  oddpwdclemodd  11886  blfvalps  12593  elblps  12598  elbl  12599  elbl3ps  12602  elbl3  12603  blres  12642  comet  12707  bdbl  12711  xmetxp  12715  xmetxpbl  12716  metcnp2  12721  txmetcnp  12726  cnbl0  12742  cnblcld  12743  bl2ioo  12750  addcncntoplem  12759  divcnap  12763  elcncf  12768  elcncf2  12769  cncfi  12773  rescncf  12776  mulc1cncf  12784  cncfco  12786  cncfmet  12787  cncfmptid  12791  addccncf  12794  cdivcncfap  12795  negcncf  12796  mulcncflem  12798  mulcncf  12799  ivthinclemlm  12820  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemdisj  12826  ivthinclemloc  12827  ivthinc  12829  limccl  12836  ellimc3apf  12837  limcdifap  12839  limcmpted  12840  limcimolemlt  12841  limcresi  12843  cnplimcim  12844  limccnpcntop  12852  limccnp2lem  12853  limccoap  12855  dvcoapbr  12879  dveflem  12895  eflt  12904  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  logltb  13003  logge0b  13019  loggt0b  13020  qdencn  13397  trilpolemlt1  13409