Theorem breq2d 4045

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 4037	. 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 1364   class class class wbr 4033

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  breqtrd  4059  sbcbr1g  4089  pofun  4347  csbfv12g  5596  isorel  5855  isocnv  5858  isotr  5863  caovordig  6089  caovordg  6091  caovord  6095  xporderlem  6289  th3qlem2  6697  phplem3g  6917  supsnti  7071  inflbti  7090  difinfinf  7167  enqdc1  7429  ltanqg  7467  ltmnqg  7468  archnqq  7484  prarloclemarch2  7486  prloc  7558  addnqprllem  7594  addlocprlemgt  7601  appdivnq  7630  mulnqprl  7635  1idprl  7657  ltexprlemloc  7674  caucvgprlemcanl  7711  cauappcvgprlemm  7712  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  cauappcvgpr  7729  archrecnq  7730  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemcl  7743  caucvgprlemladdrl  7745  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkeqj  7757  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgprpr  7779  ltposr  7830  ltasrg  7837  mulgt0sr  7845  mulextsr1lem  7847  mulextsr1  7848  prsrlt  7854  caucvgsrlemcl  7856  caucvgsrlemfv  7858  caucvgsrlembound  7861  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  caucvgsr  7869  map2psrprg  7872  pitonnlem2  7914  pitonn  7915  recidpipr  7923  axpre-ltadd  7953  axpre-mulgt0  7954  axpre-mulext  7955  axarch  7958  nntopi  7961  axcaucvglemval  7964  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  ltaddneg  8451  ltsubadd2  8460  lesubadd2  8462  ltaddsub  8463  leaddsub  8465  ltaddpos2  8480  posdif  8482  lesub1  8483  ltsub1  8485  ltnegcon1  8490  lenegcon1  8493  addge02  8500  leaddle0  8504  ltordlem  8509  possumd  8596  sublt0d  8597  apreap  8614  prodgt02  8880  prodge02  8882  ltmulgt12  8892  lemulge12  8894  ltdivmul  8903  ledivmul  8904  ltdivmul2  8905  lt2mul2div  8906  ledivmul2  8907  ltrec  8910  ltrec1  8915  ltdiv23  8919  lediv23  8920  nnge1  9013  halfpos  9222  lt2halves  9227  addltmul  9228  avglt2  9231  avgle2  9233  nnrecl  9247  zltlem1  9383  difgtsumgt  9395  nn0le2is012  9408  gtndiv  9421  qapne  9713  nnledivrp  9841  xltnegi  9910  xltadd1  9951  xsubge0  9956  xposdif  9957  xlesubadd  9958  xleaddadd  9962  divelunit  10077  eluzgtdifelfzo  10273  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemshrink  10338  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2zlemshrink  10343  rebtwn2z  10344  flqlelt  10366  flqbi  10380  2tnp1ge0ge0  10391  q2submod  10477  frec2uzltd  10495  frec2uzlt2d  10496  frec2uzf1od  10498  monoord  10577  ser3mono  10579  ser3ge0  10628  expnbnd  10755  nn0ltexp2  10801  facwordi  10832  hashunlem  10896  zfz1isolemiso  10931  seq3coll  10934  caucvgrelemcau  11145  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniq  11160  resqrexlemover  11175  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  maxleastlt  11380  minmax  11395  lemininf  11399  ltmininf  11400  xrmaxleastlt  11421  xrmaxltsup  11423  xrminmax  11430  xrmin1inf  11432  xrmin2inf  11433  xrltmininf  11435  xrlemininf  11436  climserle  11510  summodclem3  11545  summodclem2a  11546  summodc  11548  zsumdc  11549  fsum3  11552  fsum00  11627  fsumabs  11630  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  zproddc  11744  fprodseq  11748  fprodle  11805  sin01bnd  11922  cos01bnd  11923  summodnegmod  11987  modmulconst  11988  dvdsaddr  12002  dvdssub  12003  dvdssubr  12004  dvdslelemd  12008  dvdsfac  12025  dvdsmod  12027  oddp1even  12041  ltoddhalfle  12058  opoe  12060  omoe  12061  divalg2  12091  divalgmod  12092  ndvdssub  12095  ndvdsadd  12096  bitsfval  12107  bitsval  12108  bits0  12112  bitsp1  12115  bitsfzolem  12118  bitsfzo  12119  bezoutlembi  12172  dvdssqim  12191  dvdsmulgcd  12192  dvdssq  12198  nn0seqcvgd  12209  coprmdvds  12260  coprmdvds2  12261  rpmul  12266  cncongr1  12271  divgcdodd  12311  isprm6  12315  prmdvdsexp  12316  prmdvdsexpr  12318  prmfac1  12320  oddpwdclemxy  12337  oddpwdclemodd  12340  sqpweven  12343  2sqpwodd  12344  sqne2sq  12345  hashdvds  12389  phiprmpw  12390  eulerthlemh  12399  prmdiv  12403  prmdiveq  12404  odzval  12410  odzcllem  12411  odzdvds  12414  pythagtriplem11  12443  pythagtriplem13  12445  pythagtrip  12452  pceulem  12463  pczndvds2  12487  pcdvdsb  12489  pc2dvds  12499  pcz  12501  pcprmpw2  12502  dvdsprmpweq  12504  dvdsprmpweqle  12506  difsqpwdvds  12507  pcmpt  12512  prmpwdvds  12524  pockthlem  12525  4sqlem11  12570  exmidunben  12643  nninfdclemlt  12668  mulgval  13252  dvdsrtr  13657  dvdsrmul1  13658  unitnegcl  13686  unitpropdg  13704  elrhmunit  13733  zndvds0  14206  znunit  14215  psmettri2  14564  ismet2  14590  xmettri2  14597  comet  14735  ivthinclemum  14871  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  ivthinc  14879  ivthreinc  14881  limccl  14895  ellimc3apf  14896  sin0pilem2  15018  pilem3  15019  sincosq1sgn  15062  sincosq2sgn  15063  sincosq4sgn  15065  logltb  15110  logle1b  15128  loglt1b  15129  logbgt0b  15202  wilthlem1  15216  sgmval  15219  dvdsppwf1o  15225  perfect1  15234  lgslem1  15241  lgsval  15245  lgsdilem  15268  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  lgseisenlem1  15311  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem2  15323  m1lgs  15326  2lgslem1a1  15327  2lgslem1a  15329  2lgsoddprmlem2  15347  2lgsoddprmlem3  15352  2sqlem4  15359  2sqlem8a  15363