Theorem breq1d 4014

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 4007	. 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 4004

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  eqnbrtrd  4022  eqbrtrd  4026  eqbrtrdi  4043  sbcbr2g  4061  pofun  4313  fmptco  5683  isorel  5809  isocnv  5812  isotr  5817  imbrov2fvoveq  5900  caovordig  6040  caovordg  6042  caovord  6046  xporderlem  6232  reldmtpos  6254  brtposg  6255  tpostpos  6265  tposoprab  6281  th3qlem2  6638  ensn1g  6797  fndmeng  6810  xpsneng  6822  xpcomco  6826  snnen2oprc  6860  tridc  6899  fimax2gtrilemstep  6900  unsnfidcel  6920  pm54.43  7189  ccfunen  7263  ltsonq  7397  ltanqg  7399  ltmnqg  7400  archnqq  7416  prloc  7490  addnqprulem  7527  appdivnq  7562  mulnqpru  7568  mullocprlem  7569  1idpru  7590  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlem2  7659  cauappcvgprlemlim  7660  cauappcvgpr  7661  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgprlem2  7679  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnbj  7692  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  caucvgprprlemexb  7706  caucvgprprlemaddq  7707  caucvgprprlem1  7708  caucvgprprlem2  7709  ltsosr  7763  ltasrg  7769  addgt0sr  7774  mulextsr1  7780  prsrlt  7786  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  caucvgsr  7801  ltpsrprg  7802  pitonnlem2  7846  pitonn  7847  recidpipr  7855  axpre-ltadd  7885  axpre-mulext  7887  nntopi  7893  axcaucvglemval  7896  axcaucvglemcau  7897  axcaucvglemres  7898  ltaddnegr  8382  ltsubadd  8389  lesubadd  8391  ltaddsub2  8394  leaddsub2  8396  ltaddpos  8409  lesub2  8414  ltsub2  8416  ltnegcon2  8421  lenegcon2  8424  addge01  8429  subge0  8432  suble0  8433  lesub0  8436  ltordlem  8439  apreap  8544  divap0b  8640  mulgt1  8820  ltmulgt11  8821  gt0div  8827  ge0div  8828  ltmuldiv  8831  ltmuldiv2  8832  lemuldiv2  8839  ltrec  8840  lerec2  8846  ltdiv23  8849  lediv23  8850  sup3exmid  8914  addltmul  9155  avglt1  9157  avgle1  9159  div4p1lem1div2  9172  ztri3or  9296  zlem1lt  9309  zgt0ge1  9311  qapne  9639  divlt1lt  9724  divle1le  9725  xrltso  9796  xltnegi  9835  xltadd1  9876  xposdif  9882  xlesubadd  9883  xleaddadd  9887  nn0disj  10138  qavgle  10259  frec2uzf1od  10406  iseqf1olemfvp  10497  exp3vallem  10521  expap0  10550  leexp2r  10574  sqap0  10587  nn0ltexp2  10689  nn0opthlem1d  10700  hashennnuni  10759  hashunlem  10784  zfz1isolemiso  10819  seq3coll  10822  shftfvalg  10827  shftfibg  10829  shftfval  10830  shftfib  10832  shftfn  10833  2shfti  10840  shftidt2  10841  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemdecn  11021  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  abs00ap  11071  absdiflt  11101  absdifle  11102  lenegsq  11104  cau3lem  11123  minmax  11238  xrmaxltsup  11266  xrminmax  11273  xrltmininf  11278  xrlemininf  11279  clim  11289  clim2  11291  clim0  11293  clim0c  11294  climi0  11297  climuni  11301  2clim  11309  climshftlemg  11310  climshft  11312  climabs0  11315  climcn1  11316  climcn2  11317  addcn2  11318  subcn2  11319  mulcn2  11320  iser3shft  11354  climcau  11355  serf0  11360  sumeq1  11363  sumeq2  11367  sumrbdc  11387  summodclem2  11390  summodc  11391  zsumdc  11392  isumshft  11498  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodfap0  11553  prodfrecap  11554  prodfdivap  11555  ntrivcvgap  11556  ntrivcvgap0  11557  prodeq1f  11560  prodeq2w  11564  prodeq2  11565  prodrbdclem2  11581  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodntrivap  11592  fprodap0  11629  fprodrec  11637  fproddivapf  11639  fprodap0f  11644  tanaddaplem  11746  sin01bnd  11765  cos01bnd  11766  halfleoddlt  11899  gcddvds  11964  dvdssq  12032  lcmgcdlem  12077  lcmdvds  12079  isprm  12109  prmgt1  12132  isprm5lem  12141  isprm6  12147  pw2dvdslemn  12165  pw2dvdseu  12168  oddpwdclemxy  12169  oddpwdclemndvds  12171  oddpwdclemodd  12172  odzdvds  12245  pclem0  12286  pclemub  12287  pclemdc  12288  pcprecl  12289  pcprendvds  12290  pcpremul  12293  pceulem  12294  pcval  12296  pcelnn  12320  pc2dvds  12329  pcadd  12339  pcmpt  12341  prmpwdvds  12353  imasaddfnlemg  12735  blfvalps  13888  elblps  13893  elbl  13894  elbl3ps  13897  elbl3  13898  blres  13937  comet  14002  bdbl  14006  xmetxp  14010  xmetxpbl  14011  metcnp2  14016  txmetcnp  14021  cnbl0  14037  cnblcld  14038  bl2ioo  14045  addcncntoplem  14054  divcnap  14058  elcncf  14063  elcncf2  14064  cncfi  14068  rescncf  14071  mulc1cncf  14079  cncfco  14081  cncfmet  14082  cncfmptid  14086  addccncf  14089  cdivcncfap  14090  negcncf  14091  mulcncflem  14093  mulcncf  14094  ivthinclemlm  14115  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemdisj  14121  ivthinclemloc  14122  ivthinc  14124  limccl  14131  ellimc3apf  14132  limcdifap  14134  limcmpted  14135  limcimolemlt  14136  limcresi  14138  cnplimcim  14139  limccnpcntop  14147  limccnp2lem  14148  limccoap  14150  dvcoapbr  14174  dveflem  14190  eflt  14199  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  logltb  14298  logge0b  14314  loggt0b  14315  lgslem2  14405  lgslem3  14406  lgsval  14408  lgsfcl2  14410  lgsfle1  14413  lgsle1  14419  lgsdirprm  14438  lgsne0  14442  qdencn  14778  trilpolemlt1  14792