Theorem breq2d 4057

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 4049	. 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 105   = wceq 1373   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  breqtrd  4071  sbcbr1g  4101  pofun  4360  csbfv12g  5616  isorel  5879  isocnv  5882  isotr  5887  caovordig  6114  caovordg  6116  caovord  6120  xporderlem  6319  th3qlem2  6727  phplem3g  6955  supsnti  7109  inflbti  7128  difinfinf  7205  enqdc1  7477  ltanqg  7515  ltmnqg  7516  archnqq  7532  prarloclemarch2  7534  prloc  7606  addnqprllem  7642  addlocprlemgt  7649  appdivnq  7678  mulnqprl  7683  1idprl  7705  ltexprlemloc  7722  caucvgprlemcanl  7759  cauappcvgprlemm  7760  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlemlim  7776  cauappcvgpr  7777  archrecnq  7778  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemcl  7791  caucvgprlemladdrl  7793  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkeqj  7805  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  caucvgprprlem1  7824  caucvgprprlem2  7825  caucvgprpr  7827  ltposr  7878  ltasrg  7885  mulgt0sr  7893  mulextsr1lem  7895  mulextsr1  7896  prsrlt  7902  caucvgsrlemcl  7904  caucvgsrlemfv  7906  caucvgsrlembound  7909  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  caucvgsr  7917  map2psrprg  7920  pitonnlem2  7962  pitonn  7963  recidpipr  7971  axpre-ltadd  8001  axpre-mulgt0  8002  axpre-mulext  8003  axarch  8006  nntopi  8009  axcaucvglemval  8012  axcaucvglemcau  8013  axcaucvglemres  8014  axpre-suploclemres  8016  ltaddneg  8499  ltsubadd2  8508  lesubadd2  8510  ltaddsub  8511  leaddsub  8513  ltaddpos2  8528  posdif  8530  lesub1  8531  ltsub1  8533  ltnegcon1  8538  lenegcon1  8541  addge02  8548  leaddle0  8552  ltordlem  8557  possumd  8644  sublt0d  8645  apreap  8662  prodgt02  8928  prodge02  8930  ltmulgt12  8940  lemulge12  8942  ltdivmul  8951  ledivmul  8952  ltdivmul2  8953  lt2mul2div  8954  ledivmul2  8955  ltrec  8958  ltrec1  8963  ltdiv23  8967  lediv23  8968  nnge1  9061  halfpos  9270  lt2halves  9275  addltmul  9276  avglt2  9279  avgle2  9281  nnrecl  9295  zltlem1  9432  difgtsumgt  9444  nn0le2is012  9457  gtndiv  9470  qapne  9762  nnledivrp  9890  xltnegi  9959  xltadd1  10000  xsubge0  10005  xposdif  10006  xlesubadd  10007  xleaddadd  10011  divelunit  10126  eluzgtdifelfzo  10328  qtri3or  10385  exbtwnzlemstep  10392  exbtwnzlemshrink  10393  exbtwnzlemex  10394  exbtwnz  10395  rebtwn2zlemstep  10397  rebtwn2zlemshrink  10398  rebtwn2z  10399  flqlelt  10421  flqbi  10435  2tnp1ge0ge0  10446  q2submod  10532  frec2uzltd  10550  frec2uzlt2d  10551  frec2uzf1od  10553  monoord  10632  ser3mono  10634  ser3ge0  10683  expnbnd  10810  nn0ltexp2  10856  facwordi  10887  hashunlem  10951  zfz1isolemiso  10986  seq3coll  10989  caucvgrelemcau  11324  caucvgre  11325  cvg1nlemcau  11328  cvg1nlemres  11329  recvguniq  11339  resqrexlemover  11354  resqrexlemgt0  11364  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  maxleastlt  11559  minmax  11574  lemininf  11578  ltmininf  11579  xrmaxleastlt  11600  xrmaxltsup  11602  xrminmax  11609  xrmin1inf  11611  xrmin2inf  11612  xrltmininf  11614  xrlemininf  11615  climserle  11689  summodclem3  11724  summodclem2a  11725  summodc  11727  zsumdc  11728  fsum3  11731  fsum00  11806  fsumabs  11809  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  zproddc  11923  fprodseq  11927  fprodle  11984  sin01bnd  12101  cos01bnd  12102  summodnegmod  12166  modmulconst  12167  dvdsaddr  12181  dvdssub  12182  dvdssubr  12183  dvdslelemd  12187  dvdsfac  12204  dvdsmod  12206  oddp1even  12220  ltoddhalfle  12237  opoe  12239  omoe  12240  divalg2  12270  divalgmod  12271  ndvdssub  12274  ndvdsadd  12275  bitsfval  12286  bitsval  12287  bits0  12292  bitsp1  12295  bitsfzolem  12298  bitsfzo  12299  bitscmp  12302  bitsinv1lem  12305  bezoutlembi  12359  dvdssqim  12378  dvdsmulgcd  12379  dvdssq  12385  nn0seqcvgd  12396  coprmdvds  12447  coprmdvds2  12448  rpmul  12453  cncongr1  12458  divgcdodd  12498  isprm6  12502  prmdvdsexp  12503  prmdvdsexpr  12505  prmfac1  12507  oddpwdclemxy  12524  oddpwdclemodd  12527  sqpweven  12530  2sqpwodd  12531  sqne2sq  12532  hashdvds  12576  phiprmpw  12577  eulerthlemh  12586  prmdiv  12590  prmdiveq  12591  odzval  12597  odzcllem  12598  odzdvds  12601  pythagtriplem11  12630  pythagtriplem13  12632  pythagtrip  12639  pceulem  12650  pczndvds2  12674  pcdvdsb  12676  pc2dvds  12686  pcz  12688  pcprmpw2  12689  dvdsprmpweq  12691  dvdsprmpweqle  12693  difsqpwdvds  12694  pcmpt  12699  prmpwdvds  12711  pockthlem  12712  4sqlem11  12757  exmidunben  12830  nninfdclemlt  12855  mulgval  13491  dvdsrtr  13896  dvdsrmul1  13897  unitnegcl  13925  unitpropdg  13943  elrhmunit  13972  zndvds0  14445  znunit  14454  mplsubgfilemcl  14494  psmettri2  14833  ismet2  14859  xmettri2  14866  comet  15004  ivthinclemum  15140  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  ivthinc  15148  ivthreinc  15150  limccl  15164  ellimc3apf  15165  sin0pilem2  15287  pilem3  15288  sincosq1sgn  15331  sincosq2sgn  15332  sincosq4sgn  15334  logltb  15379  logle1b  15397  loglt1b  15398  logbgt0b  15471  wilthlem1  15485  sgmval  15488  dvdsppwf1o  15494  perfect1  15503  lgslem1  15510  lgsval  15514  lgsdilem  15537  lgsne0  15548  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  lgseisenlem1  15580  lgseisenlem2  15581  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem2  15592  m1lgs  15595  2lgslem1a1  15596  2lgslem1a  15598  2lgsoddprmlem2  15616  2lgsoddprmlem3  15621  2sqlem4  15628  2sqlem8a  15632