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  10047  exp3vallem  10071  expap0  10100  leexp2r  10124  sqap0  10136  nn0opthlem1d  10243  hashennnuni  10302  hashunlem  10327  zfz1isolemiso  10359  seq3coll  10362  shftfvalg  10367  shftfibg  10369  shftfval  10370  shftfib  10372  shftfn  10373  2shfti  10380  shftidt2  10381  caucvgre  10529  cvg1nlemcau  10532  cvg1nlemres  10533  resqrexlemdecn  10560  resqrexlemoverl  10569  resqrexlemglsq  10570  resqrexlemsqa  10572  resqrexlemex  10573  abs00ap  10610  absdiflt  10640  absdifle  10641  lenegsq  10643  cau3lem  10662  minmax  10776  xrmaxltsup  10801  xrminmax  10808  xrltmininf  10813  xrlemininf  10814  clim  10824  clim2  10826  clim0  10828  clim0c  10829  climi0  10832  climuni  10836  2clim  10844  climshftlemg  10845  climshft  10847  climabs0  10850  climcn1  10851  climcn2  10852  addcn2  10853  subcn2  10854  mulcn2  10855  iser3shft  10889  climcau  10890  serf0  10895  sumeq1  10898  sumeq2  10902  sumrbdc  10921  summodclem2  10925  summodc  10926  zsumdc  10927  isumshft  11033  mertenslemi1  11078  mertenslem2  11079  mertensabs  11080  tanaddaplem  11178  sin01bnd  11197  cos01bnd  11198  halfleoddlt  11321  gcddvds  11382  dvdssq  11447  lcmgcdlem  11486  lcmdvds  11488  isprm  11518  prmgt1  11540  isprm6  11553  pw2dvdslemn  11570  pw2dvdseu  11573  oddpwdclemxy  11574  oddpwdclemndvds  11576  oddpwdclemodd  11577  blfvalps  12171  elblps  12176  elbl  12177  elbl3ps  12180  elbl3  12181  blres  12220  comet  12285  bdbl  12289  metcnp2  12295  cnbl0  12313  cnblcld  12314  bl2ioo  12318  elcncf  12328  elcncf2  12329  cncfi  12333  rescncf  12336  mulc1cncf  12344  cncfco  12346  cncfmet  12347  cncfmptid  12349  addccncf  12351  cdivcncfap  12352  negcncf  12353  mulcncflem  12355  mulcncf  12356  limccl  12361  ellimc3ap  12362  limcdifap  12363  limcresi  12364  qdencn  12629