Theorem breq1d 4140

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 4133	. 2 |- ( A = B -> ( A R C <-> B R C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A R C <-> B R C ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  eqnbrtrd  4148  eqbrtrd  4152  eqbrtrdi  4169  sbcbr2g  4188  pofun  4457  fmptco  5874  isorel  6014  isocnv  6017  isotr  6022  imbrov2fvoveq  6110  caovordig  6255  caovordg  6257  caovord  6261  xporderlem  6467  reldmtpos  6524  brtposg  6525  tpostpos  6535  tposoprab  6551  th3qlem2  6912  ensn1g  7084  fndmeng  7098  xpsneng  7120  xpcomco  7124  snnen2oprc  7161  tridc  7204  fimax2gtrilemstep  7205  unsnfidcel  7228  pm54.43  7537  pr1or2  7541  ccfunen  7631  ltsonq  7766  ltanqg  7768  ltmnqg  7769  archnqq  7785  prloc  7859  addnqprulem  7896  appdivnq  7931  mulnqpru  7937  mullocprlem  7938  1idpru  7959  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlem2  8028  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlemexb  8075  caucvgprprlemaddq  8076  caucvgprprlem1  8077  caucvgprprlem2  8078  ltsosr  8132  ltasrg  8138  addgt0sr  8143  mulextsr1  8149  prsrlt  8155  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  caucvgsr  8170  ltpsrprg  8171  pitonnlem2  8215  pitonn  8216  recidpipr  8224  axpre-ltadd  8254  axpre-mulext  8256  nntopi  8262  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  ltaddnegr  8755  ltsubadd  8762  lesubadd  8764  ltaddsub2  8767  leaddsub2  8769  ltaddpos  8782  lesub2  8787  ltsub2  8789  ltnegcon2  8794  lenegcon2  8797  addge01  8802  subge0  8805  suble0  8806  lesub0  8809  ltordlem  8812  apreap  8918  divap0b  9016  mulgt1  9196  ltmulgt11  9197  gt0div  9203  ge0div  9204  ltmuldiv  9207  ltmuldiv2  9208  lemuldiv2  9215  ltrec  9216  lerec2  9222  ltdiv23  9225  lediv23  9226  sup3exmid  9290  addltmul  9547  avglt1  9549  avgle1  9551  div4p1lem1div2  9564  ztri3or  9692  zlem1lt  9706  zgt0ge1  9708  qapne  10049  irrmulap  10059  divlt1lt  10136  divle1le  10137  xrltso  10209  xltnegi  10248  xltadd1  10289  xposdif  10295  xlesubadd  10296  xleaddadd  10300  nn0disj  10556  qavgle  10704  fldiv4lem1div2uz2  10756  frec2uzf1od  10858  iseqf1olemfvp  10962  seqf1oglem1  10971  exp3vallem  10992  expap0  11021  leexp2r  11045  sqap0  11058  nn0ltexp2  11163  nn0opthlem1d  11174  hashennnuni  11234  hashunlem  11260  hashf1  11303  zfz1isolemiso  11307  seq3coll  11310  swrdccatin2  11517  shftfvalg  11599  shftfibg  11601  shftfval  11602  shftfib  11604  shftfn  11605  2shfti  11612  shftidt2  11613  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemdecn  11794  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemsqa  11806  resqrexlemex  11807  abs00ap  11844  absdiflt  11875  absdifle  11876  lenegsq  11878  cau3lem  11897  fiidxsupcl  12012  minmax  12014  xrmaxltsup  12043  xrminmax  12050  xrltmininf  12055  xrlemininf  12056  clim  12066  clim2  12068  clim0  12070  clim0c  12071  climi0  12074  climuni  12078  2clim  12086  climshftlemg  12087  climshft  12089  climabs0  12092  climcn1  12093  climcn2  12094  addcn2  12095  subcn2  12096  mulcn2  12097  iser3shft  12131  climcau  12132  serf0  12137  sumeq1  12140  sumeq2  12144  sumrbdc  12165  summodclem2  12168  summodc  12169  zsumdc  12170  isumshft  12276  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodfap0  12331  prodfrecap  12332  prodfdivap  12333  ntrivcvgap  12334  ntrivcvgap0  12335  prodeq1f  12338  prodeq2w  12342  prodeq2  12343  prodrbdclem2  12359  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodntrivap  12370  fprodap0  12407  fprodrec  12415  fproddivapf  12417  fprodap0f  12422  tanaddaplem  12524  sin01bnd  12543  cos01bnd  12544  halfleoddlt  12680  gcddvds  12759  dvdssq  12827  lcmgcdlem  12874  lcmdvds  12876  isprm  12906  prmgt1  12930  isprm5lem  12939  isprm6  12945  pwbdvdslemn  12963  pwbdvdseu  12966  nnmaxpwlemxy  12967  nnmaxpwlemnfac  12970  sqrtrirr  13008  odzdvds  13047  pclem0  13088  pclemub  13089  pclemdc  13090  pcprecl  13091  pcprendvds  13092  pcpremul  13095  pceulem  13096  pcval  13098  pcelnn  13123  pc2dvds  13132  pcadd  13142  pcadd2  13143  pcmpt  13145  prmpwdvds  13157  4sqlem17  13209  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  ballotfilemic  13302  ballotfilemsv  13305  ballotfilemrc  13326  imasaddfnlemg  13688  znf1o  15070  znidomb  15077  psrbaglefifi  15147  mplsubgfilemm  15180  mplsubgfilemcl  15181  blfvalps  15577  elblps  15582  elbl  15583  elbl3ps  15586  elbl3  15587  blres  15626  comet  15691  bdbl  15695  xmetxp  15699  xmetxpbl  15700  metcnp2  15705  txmetcnp  15710  cnbl0  15726  cnblcld  15727  bl2ioo  15742  addcncntoplem  15753  divcnap  15757  mpomulcn  15758  elcncf  15765  elcncf2  15766  cncfi  15770  rescncf  15773  mulc1cncf  15781  cncfco  15783  cncfmet  15784  cncfmptid  15789  addccncf  15792  cdivcncfap  15796  negcncf  15797  mulcncflem  15799  mulcncf  15800  ivthinclemlm  15826  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  ivthinc  15835  ivthreinc  15837  limccl  15851  ellimc3apf  15852  limcdifap  15854  limcmpted  15855  limcimolemlt  15856  limcresi  15858  cnplimcim  15859  limccnpcntop  15867  limccnp2lem  15868  limccoap  15870  dvcoapbr  15899  dveflem  15918  eflt  15967  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  logltb  16068  logge0b  16084  loggt0b  16085  zprmlogbaplem2  16177  zprmlogbap  16179  pellexlem3  16192  chtublem  16256  chtqub  16257  prmefexple  16269  bposlem1  16272  bposlem6  16277  lgslem2  16286  lgslem3  16287  lgsval  16289  lgsfcl2  16291  lgsfle1  16294  lgsle1  16300  lgsdirprm  16319  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem2  16347  gausslemma2dlem3  16348  gausslemma2dlem4  16349  subupgr  16680  vtxdumgrfival  16705  qdencn  17238  trilpolemlt1  17257