Theorem breq1d 3999

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 3992	. 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 1348   class class class wbr 3989

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  eqnbrtrd  4007  eqbrtrd  4011  eqbrtrdi  4028  sbcbr2g  4046  pofun  4297  fmptco  5662  isorel  5787  isocnv  5790  isotr  5795  imbrov2fvoveq  5878  caovordig  6018  caovordg  6020  caovord  6024  xporderlem  6210  reldmtpos  6232  brtposg  6233  tpostpos  6243  tposoprab  6259  th3qlem2  6616  ensn1g  6775  fndmeng  6788  xpsneng  6800  xpcomco  6804  snnen2oprc  6838  tridc  6877  fimax2gtrilemstep  6878  unsnfidcel  6898  pm54.43  7167  ccfunen  7226  ltsonq  7360  ltanqg  7362  ltmnqg  7363  archnqq  7379  prloc  7453  addnqprulem  7490  appdivnq  7525  mulnqpru  7531  mullocprlem  7532  1idpru  7553  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlem2  7622  cauappcvgprlemlim  7623  cauappcvgpr  7624  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlemexb  7669  caucvgprprlemaddq  7670  caucvgprprlem1  7671  caucvgprprlem2  7672  ltsosr  7726  ltasrg  7732  addgt0sr  7737  mulextsr1  7743  prsrlt  7749  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  caucvgsr  7764  ltpsrprg  7765  pitonnlem2  7809  pitonn  7810  recidpipr  7818  axpre-ltadd  7848  axpre-mulext  7850  nntopi  7856  axcaucvglemval  7859  axcaucvglemcau  7860  axcaucvglemres  7861  ltaddnegr  8344  ltsubadd  8351  lesubadd  8353  ltaddsub2  8356  leaddsub2  8358  ltaddpos  8371  lesub2  8376  ltsub2  8378  ltnegcon2  8383  lenegcon2  8386  addge01  8391  subge0  8394  suble0  8395  lesub0  8398  ltordlem  8401  apreap  8506  divap0b  8600  mulgt1  8779  ltmulgt11  8780  gt0div  8786  ge0div  8787  ltmuldiv  8790  ltmuldiv2  8791  lemuldiv2  8798  ltrec  8799  lerec2  8805  ltdiv23  8808  lediv23  8809  sup3exmid  8873  addltmul  9114  avglt1  9116  avgle1  9118  div4p1lem1div2  9131  ztri3or  9255  zlem1lt  9268  zgt0ge1  9270  qapne  9598  divlt1lt  9681  divle1le  9682  xrltso  9753  xltnegi  9792  xltadd1  9833  xposdif  9839  xlesubadd  9840  xleaddadd  9844  nn0disj  10094  qavgle  10215  frec2uzf1od  10362  iseqf1olemfvp  10453  exp3vallem  10477  expap0  10506  leexp2r  10530  sqap0  10542  nn0ltexp2  10644  nn0opthlem1d  10654  hashennnuni  10713  hashunlem  10739  zfz1isolemiso  10774  seq3coll  10777  shftfvalg  10782  shftfibg  10784  shftfval  10785  shftfib  10787  shftfn  10788  2shfti  10795  shftidt2  10796  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemdecn  10976  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  abs00ap  11026  absdiflt  11056  absdifle  11057  lenegsq  11059  cau3lem  11078  minmax  11193  xrmaxltsup  11221  xrminmax  11228  xrltmininf  11233  xrlemininf  11234  clim  11244  clim2  11246  clim0  11248  clim0c  11249  climi0  11252  climuni  11256  2clim  11264  climshftlemg  11265  climshft  11267  climabs0  11270  climcn1  11271  climcn2  11272  addcn2  11273  subcn2  11274  mulcn2  11275  iser3shft  11309  climcau  11310  serf0  11315  sumeq1  11318  sumeq2  11322  sumrbdc  11342  summodclem2  11345  summodc  11346  zsumdc  11347  isumshft  11453  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodfap0  11508  prodfrecap  11509  prodfdivap  11510  ntrivcvgap  11511  ntrivcvgap0  11512  prodeq1f  11515  prodeq2w  11519  prodeq2  11520  prodrbdclem2  11536  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodntrivap  11547  fprodap0  11584  fprodrec  11592  fproddivapf  11594  fprodap0f  11599  tanaddaplem  11701  sin01bnd  11720  cos01bnd  11721  halfleoddlt  11853  gcddvds  11918  dvdssq  11986  lcmgcdlem  12031  lcmdvds  12033  isprm  12063  prmgt1  12086  isprm5lem  12095  isprm6  12101  pw2dvdslemn  12119  pw2dvdseu  12122  oddpwdclemxy  12123  oddpwdclemndvds  12125  oddpwdclemodd  12126  odzdvds  12199  pclem0  12240  pclemub  12241  pclemdc  12242  pcprecl  12243  pcprendvds  12244  pcpremul  12247  pceulem  12248  pcval  12250  pcelnn  12274  pc2dvds  12283  pcadd  12293  pcmpt  12295  prmpwdvds  12307  blfvalps  13179  elblps  13184  elbl  13185  elbl3ps  13188  elbl3  13189  blres  13228  comet  13293  bdbl  13297  xmetxp  13301  xmetxpbl  13302  metcnp2  13307  txmetcnp  13312  cnbl0  13328  cnblcld  13329  bl2ioo  13336  addcncntoplem  13345  divcnap  13349  elcncf  13354  elcncf2  13355  cncfi  13359  rescncf  13362  mulc1cncf  13370  cncfco  13372  cncfmet  13373  cncfmptid  13377  addccncf  13380  cdivcncfap  13381  negcncf  13382  mulcncflem  13384  mulcncf  13385  ivthinclemlm  13406  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  ivthinc  13415  limccl  13422  ellimc3apf  13423  limcdifap  13425  limcmpted  13426  limcimolemlt  13427  limcresi  13429  cnplimcim  13430  limccnpcntop  13438  limccnp2lem  13439  limccoap  13441  dvcoapbr  13465  dveflem  13481  eflt  13490  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  logltb  13589  logge0b  13605  loggt0b  13606  lgslem2  13696  lgslem3  13697  lgsval  13699  lgsfcl2  13701  lgsfle1  13704  lgsle1  13710  lgsdirprm  13729  lgsne0  13733  qdencn  14059  trilpolemlt1  14073