Theorem breq1d 3939

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 3932	. 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 1331   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  eqbrtrd  3950  eqbrtrdi  3967  sbcbr2g  3985  pofun  4234  fmptco  5586  isorel  5709  isocnv  5712  isotr  5717  imbrov2fvoveq  5799  caovordig  5936  caovordg  5938  caovord  5942  xporderlem  6128  reldmtpos  6150  brtposg  6151  tpostpos  6161  tposoprab  6177  th3qlem2  6532  ensn1g  6691  fndmeng  6704  xpsneng  6716  xpcomco  6720  snnen2oprc  6754  tridc  6793  fimax2gtrilemstep  6794  unsnfidcel  6809  pm54.43  7046  ccfunen  7079  ltsonq  7206  ltanqg  7208  ltmnqg  7209  archnqq  7225  prloc  7299  addnqprulem  7336  appdivnq  7371  mulnqpru  7377  mullocprlem  7378  1idpru  7399  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlem2  7468  cauappcvgprlemlim  7469  cauappcvgpr  7470  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgprlem2  7488  caucvgpr  7490  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnbj  7501  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexbt  7514  caucvgprprlemexb  7515  caucvgprprlemaddq  7516  caucvgprprlem1  7517  caucvgprprlem2  7518  ltsosr  7572  ltasrg  7578  addgt0sr  7583  mulextsr1  7589  prsrlt  7595  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  caucvgsr  7610  ltpsrprg  7611  pitonnlem2  7655  pitonn  7656  recidpipr  7664  axpre-ltadd  7694  axpre-mulext  7696  nntopi  7702  axcaucvglemval  7705  axcaucvglemcau  7706  axcaucvglemres  7707  ltaddnegr  8187  ltsubadd  8194  lesubadd  8196  ltaddsub2  8199  leaddsub2  8201  ltaddpos  8214  lesub2  8219  ltsub2  8221  ltnegcon2  8226  lenegcon2  8229  addge01  8234  subge0  8237  suble0  8238  lesub0  8241  ltordlem  8244  apreap  8349  divap0b  8443  mulgt1  8621  ltmulgt11  8622  gt0div  8628  ge0div  8629  ltmuldiv  8632  ltmuldiv2  8633  lemuldiv2  8640  ltrec  8641  lerec2  8647  ltdiv23  8650  lediv23  8651  sup3exmid  8715  addltmul  8956  avglt1  8958  avgle1  8960  div4p1lem1div2  8973  ztri3or  9097  zlem1lt  9110  zgt0ge1  9112  qapne  9431  divlt1lt  9511  divle1le  9512  xrltso  9582  xltnegi  9618  xltadd1  9659  xposdif  9665  xlesubadd  9666  xleaddadd  9670  nn0disj  9915  qavgle  10036  frec2uzf1od  10179  iseqf1olemfvp  10270  exp3vallem  10294  expap0  10323  leexp2r  10347  sqap0  10359  nn0opthlem1d  10466  hashennnuni  10525  hashunlem  10550  zfz1isolemiso  10582  seq3coll  10585  shftfvalg  10590  shftfibg  10592  shftfval  10593  shftfib  10595  shftfn  10596  2shfti  10603  shftidt2  10604  caucvgre  10753  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemdecn  10784  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  abs00ap  10834  absdiflt  10864  absdifle  10865  lenegsq  10867  cau3lem  10886  minmax  11001  xrmaxltsup  11027  xrminmax  11034  xrltmininf  11039  xrlemininf  11040  clim  11050  clim2  11052  clim0  11054  clim0c  11055  climi0  11058  climuni  11062  2clim  11070  climshftlemg  11071  climshft  11073  climabs0  11076  climcn1  11077  climcn2  11078  addcn2  11079  subcn2  11080  mulcn2  11081  iser3shft  11115  climcau  11116  serf0  11121  sumeq1  11124  sumeq2  11128  sumrbdc  11148  summodclem2  11151  summodc  11152  zsumdc  11153  isumshft  11259  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodfap0  11314  prodfrecap  11315  prodfdivap  11316  ntrivcvgap  11317  ntrivcvgap0  11318  prodeq1f  11321  prodeq2w  11325  prodeq2  11326  prodrbdclem2  11342  prodmodclem2  11346  prodmodc  11347  tanaddaplem  11445  sin01bnd  11464  cos01bnd  11465  halfleoddlt  11591  gcddvds  11652  dvdssq  11719  lcmgcdlem  11758  lcmdvds  11760  isprm  11790  prmgt1  11812  isprm6  11825  pw2dvdslemn  11843  pw2dvdseu  11846  oddpwdclemxy  11847  oddpwdclemndvds  11849  oddpwdclemodd  11850  blfvalps  12554  elblps  12559  elbl  12560  elbl3ps  12563  elbl3  12564  blres  12603  comet  12668  bdbl  12672  xmetxp  12676  xmetxpbl  12677  metcnp2  12682  txmetcnp  12687  cnbl0  12703  cnblcld  12704  bl2ioo  12711  addcncntoplem  12720  divcnap  12724  elcncf  12729  elcncf2  12730  cncfi  12734  rescncf  12737  mulc1cncf  12745  cncfco  12747  cncfmet  12748  cncfmptid  12752  addccncf  12755  cdivcncfap  12756  negcncf  12757  mulcncflem  12759  mulcncf  12760  ivthinclemlm  12781  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemdisj  12787  ivthinclemloc  12788  ivthinc  12790  limccl  12797  ellimc3apf  12798  limcdifap  12800  limcmpted  12801  limcimolemlt  12802  limcresi  12804  cnplimcim  12805  limccnpcntop  12813  limccnp2lem  12814  limccoap  12816  dvcoapbr  12840  dveflem  12855  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  qdencn  13222  trilpolemlt1  13234