Theorem breq2d 3907

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 3899	. 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 104   = wceq 1314   class class class wbr 3895

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-br 3896

This theorem is referenced by:  breqtrd  3919  sbcbr1g  3946  pofun  4194  csbfv12g  5411  isorel  5663  isocnv  5666  isotr  5671  caovordig  5890  caovordg  5892  caovord  5896  xporderlem  6082  th3qlem2  6486  phplem3g  6703  supsnti  6844  inflbti  6863  difinfinf  6938  enqdc1  7118  ltanqg  7156  ltmnqg  7157  archnqq  7173  prarloclemarch2  7175  prloc  7247  addnqprllem  7283  addlocprlemgt  7290  appdivnq  7319  mulnqprl  7324  1idprl  7346  ltexprlemloc  7363  caucvgprlemcanl  7400  cauappcvgprlemm  7401  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  cauappcvgprlem1  7415  cauappcvgprlemlim  7417  cauappcvgpr  7418  archrecnq  7419  caucvgprlemnkj  7422  caucvgprlemnbj  7423  caucvgprlemm  7424  caucvgprlemcl  7432  caucvgprlemladdrl  7434  caucvgpr  7438  caucvgprprlemell  7441  caucvgprprlemelu  7442  caucvgprprlemcbv  7443  caucvgprprlemval  7444  caucvgprprlemnkeqj  7446  caucvgprprlemml  7450  caucvgprprlemmu  7451  caucvgprprlemopl  7453  caucvgprprlemlol  7454  caucvgprprlemopu  7455  caucvgprprlemloc  7459  caucvgprprlemclphr  7461  caucvgprprlemexbt  7462  caucvgprprlem1  7465  caucvgprprlem2  7466  caucvgprpr  7468  ltposr  7506  ltasrg  7513  mulgt0sr  7520  mulextsr1lem  7522  mulextsr1  7523  prsrlt  7529  caucvgsrlemcl  7531  caucvgsrlemfv  7533  caucvgsrlembound  7536  caucvgsrlemgt1  7537  caucvgsrlemoffres  7542  caucvgsr  7544  pitonnlem2  7582  pitonn  7583  recidpipr  7591  axpre-ltadd  7621  axpre-mulgt0  7622  axpre-mulext  7623  axarch  7626  nntopi  7629  axcaucvglemval  7632  axcaucvglemcau  7633  axcaucvglemres  7634  ltaddneg  8105  ltsubadd2  8114  lesubadd2  8116  ltaddsub  8117  leaddsub  8119  ltaddpos2  8134  posdif  8136  lesub1  8137  ltsub1  8139  ltnegcon1  8144  lenegcon1  8147  addge02  8154  leaddle0  8158  ltordlem  8163  possumd  8249  sublt0d  8250  apreap  8267  prodgt02  8521  prodge02  8523  ltmulgt12  8533  lemulge12  8535  ltdivmul  8544  ledivmul  8545  ltdivmul2  8546  lt2mul2div  8547  ledivmul2  8548  ltrec  8551  ltrec1  8556  ltdiv23  8560  lediv23  8561  nnge1  8653  halfpos  8855  lt2halves  8859  addltmul  8860  avglt2  8863  avgle2  8865  nnrecl  8879  zltlem1  9015  nn0le2is012  9037  gtndiv  9050  qapne  9333  nnledivrp  9446  xltnegi  9511  xltadd1  9552  xsubge0  9557  xposdif  9558  xlesubadd  9559  xleaddadd  9563  divelunit  9678  eluzgtdifelfzo  9867  qtri3or  9913  exbtwnzlemstep  9918  exbtwnzlemshrink  9919  exbtwnzlemex  9920  exbtwnz  9921  rebtwn2zlemstep  9923  rebtwn2zlemshrink  9924  rebtwn2z  9925  flqlelt  9942  flqbi  9956  2tnp1ge0ge0  9967  q2submod  10051  frec2uzltd  10069  frec2uzlt2d  10070  frec2uzf1od  10072  monoord  10142  ser3mono  10144  ser3ge0  10183  expnbnd  10308  facwordi  10379  hashunlem  10443  zfz1isolemiso  10475  seq3coll  10478  caucvgrelemcau  10644  caucvgre  10645  cvg1nlemcau  10648  cvg1nlemres  10649  recvguniq  10659  resqrexlemover  10674  resqrexlemgt0  10684  resqrexlemoverl  10685  resqrexlemglsq  10686  resqrexlemsqa  10688  resqrexlemex  10689  maxleastlt  10879  minmax  10893  lemininf  10897  ltmininf  10898  xrmaxleastlt  10917  xrmaxltsup  10919  xrminmax  10926  xrmin1inf  10928  xrmin2inf  10929  xrltmininf  10931  xrlemininf  10932  climserle  11006  summodclem3  11041  summodclem2a  11042  summodc  11044  zsumdc  11045  fsum3  11048  fsum00  11123  fsumabs  11126  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  sin01bnd  11315  cos01bnd  11316  summodnegmod  11372  modmulconst  11373  dvdsaddr  11385  dvdssub  11386  dvdssubr  11387  dvdslelemd  11389  dvdsfac  11406  dvdsmod  11408  oddp1even  11421  ltoddhalfle  11438  opoe  11440  omoe  11441  divalg2  11471  divalgmod  11472  ndvdssub  11475  ndvdsadd  11476  bezoutlembi  11539  dvdssqim  11558  dvdsmulgcd  11559  dvdssq  11565  nn0seqcvgd  11568  coprmdvds  11619  coprmdvds2  11620  rpmul  11625  cncongr1  11630  divgcdodd  11667  isprm6  11671  prmdvdsexp  11672  prmdvdsexpr  11674  prmfac1  11676  oddpwdclemxy  11692  oddpwdclemodd  11695  sqpweven  11698  2sqpwodd  11699  sqne2sq  11700  hashdvds  11742  phiprmpw  11743  exmidunben  11784  psmettri2  12317  ismet2  12343  xmettri2  12350  comet  12488  limccl  12584  ellimc3apf  12585