Theorem breq1d 3877

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 3870	. 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 1296   class class class wbr 3867

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868

This theorem is referenced by:  eqbrtrd  3887  syl6eqbr  3904  sbcbr2g  3919  pofun  4163  fmptco  5503  isorel  5625  isocnv  5628  isotr  5633  imbrov2fvoveq  5715  caovordig  5848  caovordg  5850  caovord  5854  xporderlem  6034  reldmtpos  6056  brtposg  6057  tpostpos  6067  tposoprab  6083  th3qlem2  6435  ensn1g  6594  fndmeng  6607  xpsneng  6618  xpcomco  6622  snnen2oprc  6656  tridc  6695  fimax2gtrilemstep  6696  unsnfidcel  6711  pm54.43  6915  ltsonq  7054  ltanqg  7056  ltmnqg  7057  archnqq  7073  prloc  7147  addnqprulem  7184  appdivnq  7219  mulnqpru  7225  mullocprlem  7226  1idpru  7247  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlemladdfl  7311  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlem1  7315  cauappcvgprlem2  7316  cauappcvgprlemlim  7317  cauappcvgpr  7318  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlem1  7335  caucvgprlem2  7336  caucvgpr  7338  caucvgprprlemell  7341  caucvgprprlemelu  7342  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemnkltj  7345  caucvgprprlemnkeqj  7346  caucvgprprlemnbj  7349  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgprprlemexb  7363  caucvgprprlemaddq  7364  caucvgprprlem1  7365  caucvgprprlem2  7366  ltsosr  7407  ltasrg  7413  addgt0sr  7418  mulextsr1  7423  prsrlt  7429  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  caucvgsr  7444  pitonnlem2  7481  pitonn  7482  recidpipr  7490  axpre-ltadd  7518  axpre-mulext  7520  nntopi  7526  axcaucvglemval  7529  axcaucvglemcau  7530  axcaucvglemres  7531  ltaddnegr  8000  ltsubadd  8007  lesubadd  8009  ltaddsub2  8012  leaddsub2  8014  ltaddpos  8027  lesub2  8032  ltsub2  8034  ltnegcon2  8039  lenegcon2  8042  addge01  8047  subge0  8050  suble0  8051  lesub0  8054  ltordlem  8057  apreap  8161  divap0b  8247  mulgt1  8421  ltmulgt11  8422  gt0div  8428  ge0div  8429  ltmuldiv  8432  ltmuldiv2  8433  lemuldiv2  8440  ltrec  8441  lerec2  8447  ltdiv23  8450  lediv23  8451  sup3exmid  8515  addltmul  8750  avglt1  8752  avgle1  8754  div4p1lem1div2  8767  ztri3or  8891  zlem1lt  8904  zgt0ge1  8906  qapne  9223  divlt1lt  9300  divle1le  9301  xrltso  9365  xltnegi  9401  xltadd1  9442  xposdif  9448  xlesubadd  9449  xleaddadd  9453  nn0disj  9698  qavgle  9819  frec2uzf1od  9962  iseqf1olemfvp  10063  exp3vallem  10087  expap0  10116  leexp2r  10140  sqap0  10152  nn0opthlem1d  10259  hashennnuni  10318  hashunlem  10343  zfz1isolemiso  10375  seq3coll  10378  shftfvalg  10383  shftfibg  10385  shftfval  10386  shftfib  10388  shftfn  10389  2shfti  10396  shftidt2  10397  caucvgre  10545  cvg1nlemcau  10548  cvg1nlemres  10549  resqrexlemdecn  10576  resqrexlemoverl  10585  resqrexlemglsq  10586  resqrexlemsqa  10588  resqrexlemex  10589  abs00ap  10626  absdiflt  10656  absdifle  10657  lenegsq  10659  cau3lem  10678  minmax  10792  xrmaxltsup  10817  xrminmax  10824  xrltmininf  10829  xrlemininf  10830  clim  10840  clim2  10842  clim0  10844  clim0c  10845  climi0  10848  climuni  10852  2clim  10860  climshftlemg  10861  climshft  10863  climabs0  10866  climcn1  10867  climcn2  10868  addcn2  10869  subcn2  10870  mulcn2  10871  iser3shft  10904  climcau  10905  serf0  10910  sumeq1  10913  sumeq2  10917  sumrbdc  10936  summodclem2  10940  summodc  10941  zsumdc  10942  isumshft  11048  mertenslemi1  11093  mertenslem2  11094  mertensabs  11095  tanaddaplem  11193  sin01bnd  11212  cos01bnd  11213  halfleoddlt  11336  gcddvds  11397  dvdssq  11462  lcmgcdlem  11501  lcmdvds  11503  isprm  11533  prmgt1  11555  isprm6  11568  pw2dvdslemn  11585  pw2dvdseu  11588  oddpwdclemxy  11589  oddpwdclemndvds  11591  oddpwdclemodd  11592  blfvalps  12186  elblps  12191  elbl  12192  elbl3ps  12195  elbl3  12196  blres  12235  comet  12300  bdbl  12304  metcnp2  12310  cnbl0  12326  cnblcld  12327  bl2ioo  12331  elcncf  12341  elcncf2  12342  cncfi  12346  rescncf  12349  mulc1cncf  12357  cncfco  12359  qdencn  12624