Theorem breq2d 4120

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 4112	. 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 4108

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109

This theorem is referenced by:  breqtrd  4134  sbcbr1g  4165  pofun  4432  csbfv12g  5709  isorel  5980  isocnv  5983  isotr  5988  caovordig  6219  caovordg  6221  caovord  6225  xporderlem  6426  th3qlem2  6871  phplem3g  7109  supsnti  7295  inflbti  7314  difinfinf  7391  enqdc1  7673  ltanqg  7711  ltmnqg  7712  archnqq  7728  prarloclemarch2  7730  prloc  7802  addnqprllem  7838  addlocprlemgt  7845  appdivnq  7874  mulnqprl  7879  1idprl  7901  ltexprlemloc  7918  caucvgprlemcanl  7955  cauappcvgprlemm  7956  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  cauappcvgprlem1  7970  cauappcvgprlemlim  7972  cauappcvgpr  7973  archrecnq  7974  caucvgprlemnkj  7977  caucvgprlemnbj  7978  caucvgprlemm  7979  caucvgprlemcl  7987  caucvgprlemladdrl  7989  caucvgpr  7993  caucvgprprlemell  7996  caucvgprprlemelu  7997  caucvgprprlemcbv  7998  caucvgprprlemval  7999  caucvgprprlemnkeqj  8001  caucvgprprlemml  8005  caucvgprprlemmu  8006  caucvgprprlemopl  8008  caucvgprprlemlol  8009  caucvgprprlemopu  8010  caucvgprprlemloc  8014  caucvgprprlemclphr  8016  caucvgprprlemexbt  8017  caucvgprprlem1  8020  caucvgprprlem2  8021  caucvgprpr  8023  ltposr  8074  ltasrg  8081  mulgt0sr  8089  mulextsr1lem  8091  mulextsr1  8092  prsrlt  8098  caucvgsrlemcl  8100  caucvgsrlemfv  8102  caucvgsrlembound  8105  caucvgsrlemgt1  8106  caucvgsrlemoffres  8111  caucvgsr  8113  map2psrprg  8116  pitonnlem2  8158  pitonn  8159  recidpipr  8167  axpre-ltadd  8197  axpre-mulgt0  8198  axpre-mulext  8199  axarch  8202  nntopi  8205  axcaucvglemval  8208  axcaucvglemcau  8209  axcaucvglemres  8210  axpre-suploclemres  8212  ltaddneg  8694  ltsubadd2  8703  lesubadd2  8705  ltaddsub  8706  leaddsub  8708  ltaddpos2  8723  posdif  8725  lesub1  8726  ltsub1  8728  ltnegcon1  8733  lenegcon1  8736  addge02  8743  leaddle0  8747  ltordlem  8752  possumd  8839  sublt0d  8840  apreap  8857  prodgt02  9123  prodge02  9125  ltmulgt12  9135  lemulge12  9137  ltdivmul  9146  ledivmul  9147  ltdivmul2  9148  lt2mul2div  9149  ledivmul2  9150  ltrec  9153  ltrec1  9158  ltdiv23  9162  lediv23  9163  nnge1  9256  halfpos  9465  lt2halves  9470  addltmul  9471  avglt2  9474  avgle2  9476  nnrecl  9490  zltlem1  9631  difgtsumgt  9643  nn0le2is012  9656  gtndiv  9669  qapne  9967  nnledivrp  10095  xltnegi  10164  xltadd1  10205  xsubge0  10210  xposdif  10211  xlesubadd  10212  xleaddadd  10216  divelunit  10331  eluzgtdifelfzo  10538  qtri3or  10596  exbtwnzlemstep  10603  exbtwnzlemshrink  10604  exbtwnzlemex  10605  exbtwnz  10606  rebtwn2zlemstep  10608  rebtwn2zlemshrink  10609  rebtwn2z  10610  flqlelt  10632  flqbi  10646  2tnp1ge0ge0  10657  q2submod  10743  frec2uzltd  10761  frec2uzlt2d  10762  frec2uzf1od  10764  monoord  10843  ser3mono  10845  ser3ge0  10894  expnbnd  11021  nn0ltexp2  11067  facwordi  11098  hashunlem  11163  ssenneg  11197  zfz1isolemiso  11204  seq3coll  11207  swrdccat3blem  11424  caucvgrelemcau  11658  caucvgre  11659  cvg1nlemcau  11662  cvg1nlemres  11663  recvguniq  11673  resqrexlemover  11688  resqrexlemgt0  11698  resqrexlemoverl  11699  resqrexlemglsq  11700  resqrexlemsqa  11702  resqrexlemex  11703  maxleastlt  11893  minmax  11908  lemininf  11912  ltmininf  11913  xrmaxleastlt  11934  xrmaxltsup  11936  xrminmax  11943  xrmin1inf  11945  xrmin2inf  11946  xrltmininf  11948  xrlemininf  11949  climserle  12023  summodclem3  12059  summodclem2a  12060  summodc  12062  zsumdc  12063  fsum3  12066  fsum00  12141  fsumabs  12144  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  zproddc  12258  fprodseq  12262  fprodle  12319  sin01bnd  12436  cos01bnd  12437  summodnegmod  12501  modmulconst  12502  dvdsaddr  12516  dvdssub  12517  dvdssubr  12518  dvdslelemd  12522  dvdsfac  12539  dvdsmod  12541  oddp1even  12555  ltoddhalfle  12572  opoe  12574  omoe  12575  divalg2  12605  divalgmod  12606  ndvdssub  12609  ndvdsadd  12610  bitsfval  12621  bitsval  12622  bits0  12627  bitsp1  12630  bitsfzolem  12633  bitsfzo  12634  bitscmp  12637  bitsinv1lem  12640  bezoutlembi  12694  dvdssqim  12713  dvdsmulgcd  12714  dvdssq  12720  nn0seqcvgd  12731  coprmdvds  12782  coprmdvds2  12783  rpmul  12788  cncongr1  12793  divgcdodd  12833  isprm6  12837  prmdvdsexp  12838  prmdvdsexpr  12840  prmfac1  12842  oddpwdclemxy  12859  oddpwdclemodd  12862  sqpweven  12865  2sqpwodd  12866  sqne2sq  12867  hashdvds  12911  phiprmpw  12912  eulerthlemh  12921  prmdiv  12925  prmdiveq  12926  odzval  12932  odzcllem  12933  odzdvds  12936  pythagtriplem11  12965  pythagtriplem13  12967  pythagtrip  12974  pceulem  12985  pczndvds2  13009  pcdvdsb  13011  pc2dvds  13021  pcz  13023  pcprmpw2  13024  dvdsprmpweq  13026  dvdsprmpweqle  13028  difsqpwdvds  13029  pcmpt  13034  prmpwdvds  13046  pockthlem  13047  4sqlem11  13092  exmidunben  13166  nninfdclemlt  13191  mulgval  13828  dvdsrtr  14235  dvdsrmul1  14236  unitnegcl  14264  unitpropdg  14282  elrhmunit  14311  zndvds0  14785  znunit  14794  mplsubgfilemcl  14841  psmettri2  15180  ismet2  15206  xmettri2  15213  comet  15351  ivthinclemum  15487  ivthinclemlopn  15488  ivthinclemlr  15489  ivthinclemuopn  15490  ivthinclemur  15491  ivthinclemdisj  15492  ivthinclemloc  15493  ivthinc  15495  ivthreinc  15497  limccl  15511  ellimc3apf  15512  sin0pilem2  15634  pilem3  15635  sincosq1sgn  15678  sincosq2sgn  15679  sincosq4sgn  15681  logltb  15726  logle1b  15744  loglt1b  15745  logbgt0b  15818  wilthlem1  15835  sgmval  15838  dvdsppwf1o  15844  perfect1  15853  lgslem1  15860  lgsval  15864  lgsdilem  15887  lgsne0  15898  gausslemma2dlem1a  15918  gausslemma2dlem1f1o  15920  lgseisenlem1  15930  lgseisenlem2  15931  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2lem2  15942  m1lgs  15945  2lgslem1a1  15946  2lgslem1a  15948  2lgsoddprmlem2  15966  2lgsoddprmlem3  15971  2sqlem4  15978  2sqlem8a  15982  eupth2lem3lem3fi  16452  eupth2lem3lem6fi  16453  eupth2lem3lem4fi  16455  eupth2lem3lem7fi  16456  eupth2lemsfi  16460  eupth2fi  16461  konigsberglem4  16473