Theorem breq1d 4015

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 4008	. 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 105   = wceq 1353   class class class wbr 4005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  eqnbrtrd  4023  eqbrtrd  4027  eqbrtrdi  4044  sbcbr2g  4062  pofun  4314  fmptco  5684  isorel  5811  isocnv  5814  isotr  5819  imbrov2fvoveq  5902  caovordig  6042  caovordg  6044  caovord  6048  xporderlem  6234  reldmtpos  6256  brtposg  6257  tpostpos  6267  tposoprab  6283  th3qlem2  6640  ensn1g  6799  fndmeng  6812  xpsneng  6824  xpcomco  6828  snnen2oprc  6862  tridc  6901  fimax2gtrilemstep  6902  unsnfidcel  6922  pm54.43  7191  ccfunen  7265  ltsonq  7399  ltanqg  7401  ltmnqg  7402  archnqq  7418  prloc  7492  addnqprulem  7529  appdivnq  7564  mulnqpru  7570  mullocprlem  7571  1idpru  7592  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlem2  7661  cauappcvgprlemlim  7662  cauappcvgpr  7663  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem1  7680  caucvgprlem2  7681  caucvgpr  7683  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkltj  7690  caucvgprprlemnkeqj  7691  caucvgprprlemnbj  7694  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlemexb  7708  caucvgprprlemaddq  7709  caucvgprprlem1  7710  caucvgprprlem2  7711  ltsosr  7765  ltasrg  7771  addgt0sr  7776  mulextsr1  7782  prsrlt  7788  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  caucvgsr  7803  ltpsrprg  7804  pitonnlem2  7848  pitonn  7849  recidpipr  7857  axpre-ltadd  7887  axpre-mulext  7889  nntopi  7895  axcaucvglemval  7898  axcaucvglemcau  7899  axcaucvglemres  7900  ltaddnegr  8384  ltsubadd  8391  lesubadd  8393  ltaddsub2  8396  leaddsub2  8398  ltaddpos  8411  lesub2  8416  ltsub2  8418  ltnegcon2  8423  lenegcon2  8426  addge01  8431  subge0  8434  suble0  8435  lesub0  8438  ltordlem  8441  apreap  8546  divap0b  8642  mulgt1  8822  ltmulgt11  8823  gt0div  8829  ge0div  8830  ltmuldiv  8833  ltmuldiv2  8834  lemuldiv2  8841  ltrec  8842  lerec2  8848  ltdiv23  8851  lediv23  8852  sup3exmid  8916  addltmul  9157  avglt1  9159  avgle1  9161  div4p1lem1div2  9174  ztri3or  9298  zlem1lt  9311  zgt0ge1  9313  qapne  9641  divlt1lt  9726  divle1le  9727  xrltso  9798  xltnegi  9837  xltadd1  9878  xposdif  9884  xlesubadd  9885  xleaddadd  9889  nn0disj  10140  qavgle  10261  frec2uzf1od  10408  iseqf1olemfvp  10499  exp3vallem  10523  expap0  10552  leexp2r  10576  sqap0  10589  nn0ltexp2  10691  nn0opthlem1d  10702  hashennnuni  10761  hashunlem  10786  zfz1isolemiso  10821  seq3coll  10824  shftfvalg  10829  shftfibg  10831  shftfval  10832  shftfib  10834  shftfn  10835  2shfti  10842  shftidt2  10843  caucvgre  10992  cvg1nlemcau  10995  cvg1nlemres  10996  resqrexlemdecn  11023  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  abs00ap  11073  absdiflt  11103  absdifle  11104  lenegsq  11106  cau3lem  11125  minmax  11240  xrmaxltsup  11268  xrminmax  11275  xrltmininf  11280  xrlemininf  11281  clim  11291  clim2  11293  clim0  11295  clim0c  11296  climi0  11299  climuni  11303  2clim  11311  climshftlemg  11312  climshft  11314  climabs0  11317  climcn1  11318  climcn2  11319  addcn2  11320  subcn2  11321  mulcn2  11322  iser3shft  11356  climcau  11357  serf0  11362  sumeq1  11365  sumeq2  11369  sumrbdc  11389  summodclem2  11392  summodc  11393  zsumdc  11394  isumshft  11500  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodfap0  11555  prodfrecap  11556  prodfdivap  11557  ntrivcvgap  11558  ntrivcvgap0  11559  prodeq1f  11562  prodeq2w  11566  prodeq2  11567  prodrbdclem2  11583  prodmodclem2  11587  prodmodc  11588  zproddc  11589  fprodntrivap  11594  fprodap0  11631  fprodrec  11639  fproddivapf  11641  fprodap0f  11646  tanaddaplem  11748  sin01bnd  11767  cos01bnd  11768  halfleoddlt  11901  gcddvds  11966  dvdssq  12034  lcmgcdlem  12079  lcmdvds  12081  isprm  12111  prmgt1  12134  isprm5lem  12143  isprm6  12149  pw2dvdslemn  12167  pw2dvdseu  12170  oddpwdclemxy  12171  oddpwdclemndvds  12173  oddpwdclemodd  12174  odzdvds  12247  pclem0  12288  pclemub  12289  pclemdc  12290  pcprecl  12291  pcprendvds  12292  pcpremul  12295  pceulem  12296  pcval  12298  pcelnn  12322  pc2dvds  12331  pcadd  12341  pcmpt  12343  prmpwdvds  12355  imasaddfnlemg  12740  blfvalps  13924  elblps  13929  elbl  13930  elbl3ps  13933  elbl3  13934  blres  13973  comet  14038  bdbl  14042  xmetxp  14046  xmetxpbl  14047  metcnp2  14052  txmetcnp  14057  cnbl0  14073  cnblcld  14074  bl2ioo  14081  addcncntoplem  14090  divcnap  14094  elcncf  14099  elcncf2  14100  cncfi  14104  rescncf  14107  mulc1cncf  14115  cncfco  14117  cncfmet  14118  cncfmptid  14122  addccncf  14125  cdivcncfap  14126  negcncf  14127  mulcncflem  14129  mulcncf  14130  ivthinclemlm  14151  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemdisj  14157  ivthinclemloc  14158  ivthinc  14160  limccl  14167  ellimc3apf  14168  limcdifap  14170  limcmpted  14171  limcimolemlt  14172  limcresi  14174  cnplimcim  14175  limccnpcntop  14183  limccnp2lem  14184  limccoap  14186  dvcoapbr  14210  dveflem  14226  eflt  14235  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  logltb  14334  logge0b  14350  loggt0b  14351  lgslem2  14441  lgslem3  14442  lgsval  14444  lgsfcl2  14446  lgsfle1  14449  lgsle1  14455  lgsdirprm  14474  lgsne0  14478  qdencn  14814  trilpolemlt1  14828