Theorem breq1d 3997

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 3990	. 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 3987

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 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  eqnbrtrd  4005  eqbrtrd  4009  eqbrtrdi  4026  sbcbr2g  4044  pofun  4295  fmptco  5660  isorel  5785  isocnv  5788  isotr  5793  imbrov2fvoveq  5876  caovordig  6016  caovordg  6018  caovord  6022  xporderlem  6208  reldmtpos  6230  brtposg  6231  tpostpos  6241  tposoprab  6257  th3qlem2  6613  ensn1g  6772  fndmeng  6785  xpsneng  6797  xpcomco  6801  snnen2oprc  6835  tridc  6874  fimax2gtrilemstep  6875  unsnfidcel  6895  pm54.43  7156  ccfunen  7215  ltsonq  7349  ltanqg  7351  ltmnqg  7352  archnqq  7368  prloc  7442  addnqprulem  7479  appdivnq  7514  mulnqpru  7520  mullocprlem  7521  1idpru  7542  cauappcvgprlemm  7596  cauappcvgprlemopl  7597  cauappcvgprlemlol  7598  cauappcvgprlemdisj  7602  cauappcvgprlemloc  7603  cauappcvgprlemladdfl  7606  cauappcvgprlemladdru  7607  cauappcvgprlemladdrl  7608  cauappcvgprlem1  7610  cauappcvgprlem2  7611  cauappcvgprlemlim  7612  cauappcvgpr  7613  caucvgprlemnkj  7617  caucvgprlemnbj  7618  caucvgprlemm  7619  caucvgprlemopl  7620  caucvgprlemlol  7621  caucvgprlemdisj  7625  caucvgprlemloc  7626  caucvgprlemcl  7627  caucvgprlemladdfu  7628  caucvgprlemladdrl  7629  caucvgprlem1  7630  caucvgprlem2  7631  caucvgpr  7633  caucvgprprlemell  7636  caucvgprprlemelu  7637  caucvgprprlemcbv  7638  caucvgprprlemval  7639  caucvgprprlemnkltj  7640  caucvgprprlemnkeqj  7641  caucvgprprlemnbj  7644  caucvgprprlemml  7645  caucvgprprlemmu  7646  caucvgprprlemopl  7648  caucvgprprlemlol  7649  caucvgprprlemopu  7650  caucvgprprlemloc  7654  caucvgprprlemclphr  7656  caucvgprprlemexbt  7657  caucvgprprlemexb  7658  caucvgprprlemaddq  7659  caucvgprprlem1  7660  caucvgprprlem2  7661  ltsosr  7715  ltasrg  7721  addgt0sr  7726  mulextsr1  7732  prsrlt  7738  caucvgsrlemgt1  7746  caucvgsrlemoffres  7751  caucvgsr  7753  ltpsrprg  7754  pitonnlem2  7798  pitonn  7799  recidpipr  7807  axpre-ltadd  7837  axpre-mulext  7839  nntopi  7845  axcaucvglemval  7848  axcaucvglemcau  7849  axcaucvglemres  7850  ltaddnegr  8333  ltsubadd  8340  lesubadd  8342  ltaddsub2  8345  leaddsub2  8347  ltaddpos  8360  lesub2  8365  ltsub2  8367  ltnegcon2  8372  lenegcon2  8375  addge01  8380  subge0  8383  suble0  8384  lesub0  8387  ltordlem  8390  apreap  8495  divap0b  8589  mulgt1  8768  ltmulgt11  8769  gt0div  8775  ge0div  8776  ltmuldiv  8779  ltmuldiv2  8780  lemuldiv2  8787  ltrec  8788  lerec2  8794  ltdiv23  8797  lediv23  8798  sup3exmid  8862  addltmul  9103  avglt1  9105  avgle1  9107  div4p1lem1div2  9120  ztri3or  9244  zlem1lt  9257  zgt0ge1  9259  qapne  9587  divlt1lt  9670  divle1le  9671  xrltso  9742  xltnegi  9781  xltadd1  9822  xposdif  9828  xlesubadd  9829  xleaddadd  9833  nn0disj  10083  qavgle  10204  frec2uzf1od  10351  iseqf1olemfvp  10442  exp3vallem  10466  expap0  10495  leexp2r  10519  sqap0  10531  nn0ltexp2  10633  nn0opthlem1d  10643  hashennnuni  10702  hashunlem  10728  zfz1isolemiso  10763  seq3coll  10766  shftfvalg  10771  shftfibg  10773  shftfval  10774  shftfib  10776  shftfn  10777  2shfti  10784  shftidt2  10785  caucvgre  10934  cvg1nlemcau  10937  cvg1nlemres  10938  resqrexlemdecn  10965  resqrexlemoverl  10974  resqrexlemglsq  10975  resqrexlemsqa  10977  resqrexlemex  10978  abs00ap  11015  absdiflt  11045  absdifle  11046  lenegsq  11048  cau3lem  11067  minmax  11182  xrmaxltsup  11210  xrminmax  11217  xrltmininf  11222  xrlemininf  11223  clim  11233  clim2  11235  clim0  11237  clim0c  11238  climi0  11241  climuni  11245  2clim  11253  climshftlemg  11254  climshft  11256  climabs0  11259  climcn1  11260  climcn2  11261  addcn2  11262  subcn2  11263  mulcn2  11264  iser3shft  11298  climcau  11299  serf0  11304  sumeq1  11307  sumeq2  11311  sumrbdc  11331  summodclem2  11334  summodc  11335  zsumdc  11336  isumshft  11442  mertenslemi1  11487  mertenslem2  11488  mertensabs  11489  prodfap0  11497  prodfrecap  11498  prodfdivap  11499  ntrivcvgap  11500  ntrivcvgap0  11501  prodeq1f  11504  prodeq2w  11508  prodeq2  11509  prodrbdclem2  11525  prodmodclem2  11529  prodmodc  11530  zproddc  11531  fprodntrivap  11536  fprodap0  11573  fprodrec  11581  fproddivapf  11583  fprodap0f  11588  tanaddaplem  11690  sin01bnd  11709  cos01bnd  11710  halfleoddlt  11842  gcddvds  11907  dvdssq  11975  lcmgcdlem  12020  lcmdvds  12022  isprm  12052  prmgt1  12075  isprm5lem  12084  isprm6  12090  pw2dvdslemn  12108  pw2dvdseu  12111  oddpwdclemxy  12112  oddpwdclemndvds  12114  oddpwdclemodd  12115  odzdvds  12188  pclem0  12229  pclemub  12230  pclemdc  12231  pcprecl  12232  pcprendvds  12233  pcpremul  12236  pceulem  12237  pcval  12239  pcelnn  12263  pc2dvds  12272  pcadd  12282  pcmpt  12284  prmpwdvds  12296  blfvalps  13140  elblps  13145  elbl  13146  elbl3ps  13149  elbl3  13150  blres  13189  comet  13254  bdbl  13258  xmetxp  13262  xmetxpbl  13263  metcnp2  13268  txmetcnp  13273  cnbl0  13289  cnblcld  13290  bl2ioo  13297  addcncntoplem  13306  divcnap  13310  elcncf  13315  elcncf2  13316  cncfi  13320  rescncf  13323  mulc1cncf  13331  cncfco  13333  cncfmet  13334  cncfmptid  13338  addccncf  13341  cdivcncfap  13342  negcncf  13343  mulcncflem  13345  mulcncf  13346  ivthinclemlm  13367  ivthinclemlopn  13369  ivthinclemlr  13370  ivthinclemuopn  13371  ivthinclemur  13372  ivthinclemdisj  13373  ivthinclemloc  13374  ivthinc  13376  limccl  13383  ellimc3apf  13384  limcdifap  13386  limcmpted  13387  limcimolemlt  13388  limcresi  13390  cnplimcim  13391  limccnpcntop  13399  limccnp2lem  13400  limccoap  13402  dvcoapbr  13426  dveflem  13442  eflt  13451  sincosq2sgn  13503  sincosq3sgn  13504  sincosq4sgn  13505  logltb  13550  logge0b  13566  loggt0b  13567  lgslem2  13657  lgslem3  13658  lgsval  13660  lgsfcl2  13662  lgsfle1  13665  lgsle1  13671  lgsdirprm  13690  lgsne0  13694  qdencn  14021  trilpolemlt1  14035