Theorem breq1d 3991

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 3984	. 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 1343   class class class wbr 3981

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  eqnbrtrd  3999  eqbrtrd  4003  eqbrtrdi  4020  sbcbr2g  4038  pofun  4289  fmptco  5650  isorel  5775  isocnv  5778  isotr  5783  imbrov2fvoveq  5866  caovordig  6003  caovordg  6005  caovord  6009  xporderlem  6195  reldmtpos  6217  brtposg  6218  tpostpos  6228  tposoprab  6244  th3qlem2  6600  ensn1g  6759  fndmeng  6772  xpsneng  6784  xpcomco  6788  snnen2oprc  6822  tridc  6861  fimax2gtrilemstep  6862  unsnfidcel  6882  pm54.43  7142  ccfunen  7201  ltsonq  7335  ltanqg  7337  ltmnqg  7338  archnqq  7354  prloc  7428  addnqprulem  7465  appdivnq  7500  mulnqpru  7506  mullocprlem  7507  1idpru  7528  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlem2  7597  cauappcvgprlemlim  7598  cauappcvgpr  7599  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprlem2  7617  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  caucvgprprlemnbj  7630  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  caucvgprprlemexb  7644  caucvgprprlemaddq  7645  caucvgprprlem1  7646  caucvgprprlem2  7647  ltsosr  7701  ltasrg  7707  addgt0sr  7712  mulextsr1  7718  prsrlt  7724  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  caucvgsr  7739  ltpsrprg  7740  pitonnlem2  7784  pitonn  7785  recidpipr  7793  axpre-ltadd  7823  axpre-mulext  7825  nntopi  7831  axcaucvglemval  7834  axcaucvglemcau  7835  axcaucvglemres  7836  ltaddnegr  8319  ltsubadd  8326  lesubadd  8328  ltaddsub2  8331  leaddsub2  8333  ltaddpos  8346  lesub2  8351  ltsub2  8353  ltnegcon2  8358  lenegcon2  8361  addge01  8366  subge0  8369  suble0  8370  lesub0  8373  ltordlem  8376  apreap  8481  divap0b  8575  mulgt1  8754  ltmulgt11  8755  gt0div  8761  ge0div  8762  ltmuldiv  8765  ltmuldiv2  8766  lemuldiv2  8773  ltrec  8774  lerec2  8780  ltdiv23  8783  lediv23  8784  sup3exmid  8848  addltmul  9089  avglt1  9091  avgle1  9093  div4p1lem1div2  9106  ztri3or  9230  zlem1lt  9243  zgt0ge1  9245  qapne  9573  divlt1lt  9656  divle1le  9657  xrltso  9728  xltnegi  9767  xltadd1  9808  xposdif  9814  xlesubadd  9815  xleaddadd  9819  nn0disj  10069  qavgle  10190  frec2uzf1od  10337  iseqf1olemfvp  10428  exp3vallem  10452  expap0  10481  leexp2r  10505  sqap0  10517  nn0ltexp2  10619  nn0opthlem1d  10629  hashennnuni  10688  hashunlem  10713  zfz1isolemiso  10748  seq3coll  10751  shftfvalg  10756  shftfibg  10758  shftfval  10759  shftfib  10761  shftfn  10762  2shfti  10769  shftidt2  10770  caucvgre  10919  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemdecn  10950  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemsqa  10962  resqrexlemex  10963  abs00ap  11000  absdiflt  11030  absdifle  11031  lenegsq  11033  cau3lem  11052  minmax  11167  xrmaxltsup  11195  xrminmax  11202  xrltmininf  11207  xrlemininf  11208  clim  11218  clim2  11220  clim0  11222  clim0c  11223  climi0  11226  climuni  11230  2clim  11238  climshftlemg  11239  climshft  11241  climabs0  11244  climcn1  11245  climcn2  11246  addcn2  11247  subcn2  11248  mulcn2  11249  iser3shft  11283  climcau  11284  serf0  11289  sumeq1  11292  sumeq2  11296  sumrbdc  11316  summodclem2  11319  summodc  11320  zsumdc  11321  isumshft  11427  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodfap0  11482  prodfrecap  11483  prodfdivap  11484  ntrivcvgap  11485  ntrivcvgap0  11486  prodeq1f  11489  prodeq2w  11493  prodeq2  11494  prodrbdclem2  11510  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodntrivap  11521  fprodap0  11558  fprodrec  11566  fproddivapf  11568  fprodap0f  11573  tanaddaplem  11675  sin01bnd  11694  cos01bnd  11695  halfleoddlt  11827  gcddvds  11892  dvdssq  11960  lcmgcdlem  12005  lcmdvds  12007  isprm  12037  prmgt1  12060  isprm5lem  12069  isprm6  12075  pw2dvdslemn  12093  pw2dvdseu  12096  oddpwdclemxy  12097  oddpwdclemndvds  12099  oddpwdclemodd  12100  odzdvds  12173  pclem0  12214  pclemub  12215  pclemdc  12216  pcprecl  12217  pcprendvds  12218  pcpremul  12221  pceulem  12222  pcval  12224  pcelnn  12248  pc2dvds  12257  pcadd  12267  pcmpt  12269  prmpwdvds  12281  blfvalps  12985  elblps  12990  elbl  12991  elbl3ps  12994  elbl3  12995  blres  13034  comet  13099  bdbl  13103  xmetxp  13107  xmetxpbl  13108  metcnp2  13113  txmetcnp  13118  cnbl0  13134  cnblcld  13135  bl2ioo  13142  addcncntoplem  13151  divcnap  13155  elcncf  13160  elcncf2  13161  cncfi  13165  rescncf  13168  mulc1cncf  13176  cncfco  13178  cncfmet  13179  cncfmptid  13183  addccncf  13186  cdivcncfap  13187  negcncf  13188  mulcncflem  13190  mulcncf  13191  ivthinclemlm  13212  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemdisj  13218  ivthinclemloc  13219  ivthinc  13221  limccl  13228  ellimc3apf  13229  limcdifap  13231  limcmpted  13232  limcimolemlt  13233  limcresi  13235  cnplimcim  13236  limccnpcntop  13244  limccnp2lem  13245  limccoap  13247  dvcoapbr  13271  dveflem  13287  eflt  13296  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  logltb  13395  logge0b  13411  loggt0b  13412  lgslem2  13502  lgslem3  13503  lgsval  13505  lgsfcl2  13507  lgsfle1  13510  lgsle1  13516  lgsdirprm  13535  lgsne0  13539  qdencn  13866  trilpolemlt1  13880