Theorem breq2d 4126

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 4118	. 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 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breqtrd  4140  sbcbr1g  4171  pofun  4438  csbfv12g  5715  isorel  5987  isocnv  5990  isotr  5995  caovordig  6228  caovordg  6230  caovord  6234  xporderlem  6440  th3qlem2  6885  phplem3g  7123  supsnti  7309  inflbti  7328  difinfinf  7405  enqdc1  7693  ltanqg  7731  ltmnqg  7732  archnqq  7748  prarloclemarch2  7750  prloc  7822  addnqprllem  7858  addlocprlemgt  7865  appdivnq  7894  mulnqprl  7899  1idprl  7921  ltexprlemloc  7938  caucvgprlemcanl  7975  cauappcvgprlemm  7976  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  cauappcvgpr  7993  archrecnq  7994  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgprpr  8043  ltposr  8094  ltasrg  8101  mulgt0sr  8109  mulextsr1lem  8111  mulextsr1  8112  prsrlt  8118  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsrlembound  8125  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  map2psrprg  8136  pitonnlem2  8178  pitonn  8179  recidpipr  8187  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axarch  8222  nntopi  8225  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  ltaddneg  8716  ltsubadd2  8725  lesubadd2  8727  ltaddsub  8728  leaddsub  8730  ltaddpos2  8745  posdif  8747  lesub1  8748  ltsub1  8750  ltnegcon1  8755  lenegcon1  8758  addge02  8765  leaddle0  8769  ltordlem  8774  possumd  8861  sublt0d  8862  apreap  8879  prodgt02  9147  prodge02  9149  ltmulgt12  9159  lemulge12  9161  ltdivmul  9170  ledivmul  9171  ltdivmul2  9172  lt2mul2div  9173  ledivmul2  9174  ltrec  9177  ltrec1  9182  ltdiv23  9186  lediv23  9187  nnge1  9280  halfpos  9489  lt2halves  9494  addltmul  9495  avglt2  9498  avgle2  9500  nnrecl  9514  zltlem1  9655  difgtsumgt  9667  nn0le2is012  9681  gtndiv  9694  qapne  9992  nnledivrp  10120  xltnegi  10190  xltadd1  10231  xsubge0  10236  xposdif  10237  xlesubadd  10238  xleaddadd  10242  divelunit  10357  eluzgtdifelfzo  10567  qtri3or  10627  exbtwnzlemstep  10634  exbtwnzlemshrink  10635  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2zlemshrink  10640  rebtwn2z  10641  flqlelt  10663  flqbi  10677  2tnp1ge0ge0  10688  q2submod  10774  frec2uzltd  10792  frec2uzlt2d  10793  frec2uzf1od  10795  monoord  10874  ser3mono  10876  ser3ge0  10925  expnbnd  11053  nn0ltexp2  11099  facwordi  11130  hashunlem  11196  ssenneg  11232  zfz1isolemiso  11239  seq3coll  11242  swrdccat3blem  11459  caucvgrelemcau  11693  caucvgre  11694  cvg1nlemcau  11697  cvg1nlemres  11698  recvguniq  11708  resqrexlemover  11723  resqrexlemgt0  11733  resqrexlemoverl  11734  resqrexlemglsq  11735  resqrexlemsqa  11737  resqrexlemex  11738  maxleastlt  11928  minmax  11943  lemininf  11947  ltmininf  11948  xrmaxleastlt  11969  xrmaxltsup  11971  xrminmax  11978  xrmin1inf  11980  xrmin2inf  11981  xrltmininf  11983  xrlemininf  11984  climserle  12058  summodclem3  12094  summodclem2a  12095  summodc  12097  zsumdc  12098  fsum3  12101  fsum00  12176  fsumabs  12179  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  zproddc  12293  fprodseq  12297  fprodle  12354  sin01bnd  12471  cos01bnd  12472  summodnegmod  12536  modmulconst  12537  dvdsaddr  12551  dvdssub  12552  dvdssubr  12553  dvdslelemd  12557  dvdsfac  12574  dvdsmod  12576  oddp1even  12590  ltoddhalfle  12607  opoe  12609  omoe  12610  divalg2  12640  divalgmod  12641  ndvdssub  12644  ndvdsadd  12645  bitsfval  12656  bitsval  12657  bits0  12662  bitsp1  12665  bitsfzolem  12668  bitsfzo  12669  bitscmp  12672  bitsinv1lem  12675  bezoutlembi  12729  dvdssqim  12748  dvdsmulgcd  12749  dvdssq  12755  nn0seqcvgd  12766  coprmdvds  12817  coprmdvds2  12818  rpmul  12823  cncongr1  12828  divgcdodd  12868  isprm6  12872  prmdvdsexp  12873  prmdvdsexpr  12875  prmfac1  12877  oddpwdclemxy  12894  oddpwdclemodd  12897  sqpweven  12900  2sqpwodd  12901  sqne2sq  12902  hashdvds  12946  phiprmpw  12947  eulerthlemh  12956  prmdiv  12960  prmdiveq  12961  odzval  12967  odzcllem  12968  odzdvds  12971  pythagtriplem11  13000  pythagtriplem13  13002  pythagtrip  13009  pceulem  13020  pczndvds2  13044  pcdvdsb  13046  pc2dvds  13056  pcz  13058  pcprmpw2  13059  dvdsprmpweq  13061  dvdsprmpweqle  13063  difsqpwdvds  13064  pcmpt  13069  prmpwdvds  13081  pockthlem  13082  4sqlem11  13127  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfileme  13183  ballotfilemefi  13184  ballotfilemodife  13187  ballotfilem4  13188  ballotfilem1c  13198  ballotfilemsval  13199  ballotfilemieq  13207  ballotfilemfrcn0  13220  ballotfi  13229  exmidunben  13264  nninfdclemlt  13289  mulgval  13878  dvdsrtr  14349  dvdsrmul1  14350  unitnegcl  14378  unitpropdg  14396  elrhmunit  14425  zndvds0  14927  znunit  14936  mplsubgfilemcl  14983  psmettri2  15322  ismet2  15348  xmettri2  15355  comet  15493  ivthinclemum  15629  ivthinclemlopn  15630  ivthinclemlr  15631  ivthinclemuopn  15632  ivthinclemur  15633  ivthinclemdisj  15634  ivthinclemloc  15635  ivthinc  15637  ivthreinc  15639  limccl  15653  ellimc3apf  15654  sin0pilem2  15776  pilem3  15777  sincosq1sgn  15820  sincosq2sgn  15821  sincosq4sgn  15823  logltb  15868  logle1b  15886  loglt1b  15887  logbgt0b  15960  wilthlem1  15977  sgmval  15980  dvdsppwf1o  15986  perfect1  15995  lgslem1  16002  lgsval  16006  lgsdilem  16029  lgsne0  16040  gausslemma2dlem1a  16060  gausslemma2dlem1f1o  16062  lgseisenlem1  16072  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2lem2  16084  m1lgs  16087  2lgslem1a1  16088  2lgslem1a  16090  2lgsoddprmlem2  16108  2lgsoddprmlem3  16113  2sqlem4  16120  2sqlem8a  16124  eupth2lem3lem3fi  16594  eupth2lem3lem6fi  16595  eupth2lem3lem4fi  16597  eupth2lem3lem7fi  16598  eupth2lemsfi  16602  eupth2fi  16603  konigsberglem4  16615