Theorem breq2d 3797

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
breq2d	|- ( ph -> ( C R A <-> C R B ) )

Proof of Theorem breq2d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq2 3789	. 2 |- ( A = B -> ( C R A <-> C R B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C R A <-> C R B ) )

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:  breqtrd  3809  sbcbr1g  3836  pofun  4067  csbfv12g  5230  isorel  5468  isocnv  5471  isotr  5476  caovordig  5686  caovordg  5688  caovord  5692  xporderlem  5872  th3qlem2  6232  phplem3g  6342  supsnti  6418  inflbti  6437  enqdc1  6552  ltanqg  6590  ltmnqg  6591  archnqq  6607  prarloclemarch2  6609  prloc  6681  addnqprllem  6717  addlocprlemgt  6724  appdivnq  6753  mulnqprl  6758  1idprl  6780  ltexprlemloc  6797  caucvgprlemcanl  6834  cauappcvgprlemm  6835  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  cauappcvgpr  6852  archrecnq  6853  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemcl  6866  caucvgprlemladdrl  6868  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgprpr  6902  ltposr  6940  ltasrg  6947  mulgt0sr  6954  mulextsr1lem  6956  mulextsr1  6957  prsrlt  6963  caucvgsrlemcl  6965  caucvgsrlemfv  6967  caucvgsrlembound  6970  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  caucvgsr  6978  pitonnlem2  7015  pitonn  7016  recidpipr  7024  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  axarch  7057  nntopi  7060  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  ltaddneg  7528  ltsubadd2  7537  lesubadd2  7539  ltaddsub  7540  leaddsub  7542  ltaddpos2  7557  posdif  7559  lesub1  7560  ltsub1  7562  ltnegcon1  7567  lenegcon1  7570  addge02  7577  leaddle0  7581  possumd  7669  sublt0d  7670  apreap  7687  prodgt02  7931  prodge02  7933  ltmulgt12  7943  lemulge12  7945  ltdivmul  7954  ledivmul  7955  ltdivmul2  7956  lt2mul2div  7957  ledivmul2  7958  ltrec  7961  ltrec1  7966  ltdiv23  7970  lediv23  7971  nnge1  8062  halfpos  8262  lt2halves  8266  addltmul  8267  avglt2  8270  avgle2  8272  nnrecl  8286  zltlem1  8408  gtndiv  8442  qapne  8724  nnledivrp  8837  xltnegi  8902  divelunit  9024  eluzgtdifelfzo  9206  qtri3or  9252  qbtwnzlemstep  9257  qbtwnzlemshrink  9258  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2zlemshrink  9262  rebtwn2z  9263  flqlelt  9278  flqbi  9292  2tnp1ge0ge0  9303  q2submod  9387  frec2uzltd  9405  frec2uzlt2d  9406  frec2uzf1od  9408  monoord  9455  isermono  9457  expnbnd  9596  facwordi  9667  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemover  9896  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  maxleastlt  10101  minmax  10112  lemininf  10115  ltmininf  10116  climserile  10183  summodnegmod  10226  modmulconst  10227  dvdsaddr  10239  dvdssub  10240  dvdssubr  10241  dvdslelemd  10243  dvdsfac  10260  dvdsmod  10262  oddp1even  10275  ltoddhalfle  10293  opoe  10295  omoe  10296  divalg2  10326  divalgmod  10327  ndvdssub  10330  ndvdsadd  10331  bezoutlembi  10394  dvdssqim  10413  dvdsmulgcd  10414  dvdssq  10420  nn0seqcvgd  10423  coprmdvds  10474  coprmdvds2  10475  rpmul  10480  cncongr1  10485  divgcdodd  10522  isprm6  10526  prmdvdsexp  10527  prmdvdsexpr  10529  prmfac1  10531  oddpwdclemxy  10547  oddpwdclemodd  10550  sqpweven  10553  2sqpwodd  10554  sqne2sq  10555