Theorem breq1d 3795

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 3788	. 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 103   = wceq 1284   class class class wbr 3785

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786

This theorem is referenced by:  eqbrtrd  3805  syl6eqbr  3822  sbcbr2g  3837  pofun  4067  fmptco  5351  isorel  5468  isocnv  5471  isotr  5476  caovordig  5686  caovordg  5688  caovord  5692  xporderlem  5872  reldmtpos  5891  brtposg  5892  tpostpos  5902  tposoprab  5918  th3qlem2  6232  ensn1g  6300  fndmeng  6312  xpsneng  6319  xpcomco  6323  snnen2oprc  6346  unsnfidcel  6386  pm54.43  6459  ltsonq  6588  ltanqg  6590  ltmnqg  6591  archnqq  6607  prloc  6681  addnqprulem  6718  appdivnq  6753  mulnqpru  6759  mullocprlem  6760  1idpru  6781  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlem2  6850  cauappcvgprlemlim  6851  cauappcvgpr  6852  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  ltsosr  6941  ltasrg  6947  addgt0sr  6952  mulextsr1  6957  prsrlt  6963  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  caucvgsr  6978  pitonnlem2  7015  pitonn  7016  recidpipr  7024  axpre-ltadd  7052  axpre-mulext  7054  nntopi  7060  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  ltaddnegr  7529  ltsubadd  7536  lesubadd  7538  ltaddsub2  7541  leaddsub2  7543  ltaddpos  7556  lesub2  7561  ltsub2  7563  ltnegcon2  7568  lenegcon2  7571  addge01  7576  subge0  7579  suble0  7580  lesub0  7583  apreap  7687  divap0b  7771  mulgt1  7941  ltmulgt11  7942  gt0div  7948  ge0div  7949  ltmuldiv  7952  ltmuldiv2  7953  lemuldiv2  7960  ltrec  7961  lerec2  7967  ltdiv23  7970  lediv23  7971  addltmul  8267  avglt1  8269  avgle1  8271  div4p1lem1div2  8284  ztri3or  8394  zlem1lt  8407  zgt0ge1  8409  qapne  8724  divlt1lt  8801  divle1le  8802  xrltso  8871  xltnegi  8902  nn0disj  9148  qavgle  9267  frec2uzf1od  9408  expivallem  9477  expap0  9506  leexp2r  9530  sqap0  9542  nn0opthlem1d  9647  shftfvalg  9706  shftfibg  9708  shftfval  9709  shftfib  9711  shftfn  9712  2shfti  9719  shftidt2  9720  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemdecn  9898  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  abs00ap  9948  absdiflt  9978  absdifle  9979  lenegsq  9981  cau3lem  10000  minmax  10112  clim  10120  clim2  10122  clim0  10124  clim0c  10125  climi0  10128  climuni  10132  2clim  10140  climshftlemg  10141  climshft  10143  climabs0  10146  climcn1  10147  climcn2  10148  addcn2  10149  subcn2  10150  mulcn2  10151  climcau  10184  serif0  10189  sumeq1  10192  halfleoddlt  10294  gcddvds  10355  dvdssq  10420  lcmgcdlem  10459  lcmdvds  10461  isprm  10491  prmgt1  10513  isprm6  10526  pw2dvdslemn  10543  pw2dvdseu  10546  oddpwdclemxy  10547  oddpwdclemndvds  10549  oddpwdclemodd  10550  qdencn  10785