Theorem breq1d 4043

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 4036	. 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 1364   class class class wbr 4033

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  eqnbrtrd  4051  eqbrtrd  4055  eqbrtrdi  4072  sbcbr2g  4090  pofun  4347  fmptco  5728  isorel  5855  isocnv  5858  isotr  5863  imbrov2fvoveq  5947  caovordig  6089  caovordg  6091  caovord  6095  xporderlem  6289  reldmtpos  6311  brtposg  6312  tpostpos  6322  tposoprab  6338  th3qlem2  6697  ensn1g  6856  fndmeng  6869  xpsneng  6881  xpcomco  6885  snnen2oprc  6921  tridc  6960  fimax2gtrilemstep  6961  unsnfidcel  6982  pm54.43  7257  ccfunen  7331  ltsonq  7465  ltanqg  7467  ltmnqg  7468  archnqq  7484  prloc  7558  addnqprulem  7595  appdivnq  7630  mulnqpru  7636  mullocprlem  7637  1idpru  7658  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlem2  7727  cauappcvgprlemlim  7728  cauappcvgpr  7729  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprlem2  7747  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnbj  7760  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  caucvgprprlemaddq  7775  caucvgprprlem1  7776  caucvgprprlem2  7777  ltsosr  7831  ltasrg  7837  addgt0sr  7842  mulextsr1  7848  prsrlt  7854  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  caucvgsr  7869  ltpsrprg  7870  pitonnlem2  7914  pitonn  7915  recidpipr  7923  axpre-ltadd  7953  axpre-mulext  7955  nntopi  7961  axcaucvglemval  7964  axcaucvglemcau  7965  axcaucvglemres  7966  ltaddnegr  8452  ltsubadd  8459  lesubadd  8461  ltaddsub2  8464  leaddsub2  8466  ltaddpos  8479  lesub2  8484  ltsub2  8486  ltnegcon2  8491  lenegcon2  8494  addge01  8499  subge0  8502  suble0  8503  lesub0  8506  ltordlem  8509  apreap  8614  divap0b  8710  mulgt1  8890  ltmulgt11  8891  gt0div  8897  ge0div  8898  ltmuldiv  8901  ltmuldiv2  8902  lemuldiv2  8909  ltrec  8910  lerec2  8916  ltdiv23  8919  lediv23  8920  sup3exmid  8984  addltmul  9228  avglt1  9230  avgle1  9232  div4p1lem1div2  9245  ztri3or  9369  zlem1lt  9382  zgt0ge1  9384  qapne  9713  irrmulap  9722  divlt1lt  9799  divle1le  9800  xrltso  9871  xltnegi  9910  xltadd1  9951  xposdif  9957  xlesubadd  9958  xleaddadd  9962  nn0disj  10213  qavgle  10348  fldiv4lem1div2uz2  10396  frec2uzf1od  10498  iseqf1olemfvp  10602  seqf1oglem1  10611  exp3vallem  10632  expap0  10661  leexp2r  10685  sqap0  10698  nn0ltexp2  10801  nn0opthlem1d  10812  hashennnuni  10871  hashunlem  10896  zfz1isolemiso  10931  seq3coll  10934  shftfvalg  10983  shftfibg  10985  shftfval  10986  shftfib  10988  shftfn  10989  2shfti  10996  shftidt2  10997  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemdecn  11177  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  abs00ap  11227  absdiflt  11257  absdifle  11258  lenegsq  11260  cau3lem  11279  minmax  11395  xrmaxltsup  11423  xrminmax  11430  xrltmininf  11435  xrlemininf  11436  clim  11446  clim2  11448  clim0  11450  clim0c  11451  climi0  11454  climuni  11458  2clim  11466  climshftlemg  11467  climshft  11469  climabs0  11472  climcn1  11473  climcn2  11474  addcn2  11475  subcn2  11476  mulcn2  11477  iser3shft  11511  climcau  11512  serf0  11517  sumeq1  11520  sumeq2  11524  sumrbdc  11544  summodclem2  11547  summodc  11548  zsumdc  11549  isumshft  11655  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodfap0  11710  prodfrecap  11711  prodfdivap  11712  ntrivcvgap  11713  ntrivcvgap0  11714  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  prodrbdclem2  11738  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodntrivap  11749  fprodap0  11786  fprodrec  11794  fproddivapf  11796  fprodap0f  11801  tanaddaplem  11903  sin01bnd  11922  cos01bnd  11923  halfleoddlt  12059  gcddvds  12130  dvdssq  12198  lcmgcdlem  12245  lcmdvds  12247  isprm  12277  prmgt1  12300  isprm5lem  12309  isprm6  12315  pw2dvdslemn  12333  pw2dvdseu  12336  oddpwdclemxy  12337  oddpwdclemndvds  12339  oddpwdclemodd  12340  odzdvds  12414  pclem0  12455  pclemub  12456  pclemdc  12457  pcprecl  12458  pcprendvds  12459  pcpremul  12462  pceulem  12463  pcval  12465  pcelnn  12490  pc2dvds  12499  pcadd  12509  pcadd2  12510  pcmpt  12512  prmpwdvds  12524  4sqlem17  12576  imasaddfnlemg  12957  znf1o  14207  znidomb  14214  blfvalps  14621  elblps  14626  elbl  14627  elbl3ps  14630  elbl3  14631  blres  14670  comet  14735  bdbl  14739  xmetxp  14743  xmetxpbl  14744  metcnp2  14749  txmetcnp  14754  cnbl0  14770  cnblcld  14771  bl2ioo  14786  addcncntoplem  14797  divcnap  14801  mpomulcn  14802  elcncf  14809  elcncf2  14810  cncfi  14814  rescncf  14817  mulc1cncf  14825  cncfco  14827  cncfmet  14828  cncfmptid  14833  addccncf  14836  cdivcncfap  14840  negcncf  14841  mulcncflem  14843  mulcncf  14844  ivthinclemlm  14870  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  ivthinc  14879  ivthreinc  14881  limccl  14895  ellimc3apf  14896  limcdifap  14898  limcmpted  14899  limcimolemlt  14900  limcresi  14902  cnplimcim  14903  limccnpcntop  14911  limccnp2lem  14912  limccoap  14914  dvcoapbr  14943  dveflem  14962  eflt  15011  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  logltb  15110  logge0b  15126  loggt0b  15127  lgslem2  15242  lgslem3  15243  lgsval  15245  lgsfcl2  15247  lgsfle1  15250  lgsle1  15256  lgsdirprm  15275  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  qdencn  15671  trilpolemlt1  15685