MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq2d Structured version   Unicode version

Theorem breq2d 4451
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
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq2 4443 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C R A  <-> 
C R B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440
This theorem is referenced by:  breqtrd  4463  sbcbr1g  4493  pofun  4805  csbfv12  5883  isorel  6197  soisores  6198  soisoi  6199  isocnv  6201  isotr  6207  f1owe  6224  caovordig  6453  caovordg  6455  caovord  6459  f1oweALT  6757  frxp  6883  xporderlem  6884  fnwelem  6888  difsnen  7592  domdifsn  7593  unfilem3  7778  domunfican  7785  marypha1lem  7885  marypha1  7886  wemapwe  8130  oef1o  8132  r1sdom  8183  sdomsdomcardi  8343  alephordi  8446  pwcdadom  8587  sornom  8648  axdclem  8890  pwcfsdom  8949  elgch  8989  winalim2  9063  rankcf  9144  inatsk  9145  pinq  9294  nqereu  9296  ltaddnq  9341  ltrnq  9346  archnq  9347  addclprlem1  9383  mulclprlem  9386  1idpr  9396  ltaprlem  9411  ltapr  9412  prlem936  9414  ltasr  9466  mulgt0sr  9471  sqgt0sr  9472  map2psrpr  9476  axpre-ltadd  9533  axpre-mulgt0  9534  axpre-sup  9535  ltsubadd2  10019  lesubadd2  10021  ltaddpos2  10039  posdif  10041  lesub1  10042  ltnegcon1  10049  lenegcon1  10052  addge02  10059  leaddle0  10063  mulge0  10066  msqge0  10070  ltordlem  10074  prodgt0  10383  prodgt02  10384  prodge02  10386  ltmulgt12  10399  lemulge12  10401  mulge0b  10408  mulle0b  10409  ltdivmul  10413  ledivmul  10414  ltdivmul2  10415  lt2mul2div  10416  ledivmul2  10417  ledivmul2OLD  10418  ltrec  10421  ltrec1  10427  ltdiv23  10431  lediv23  10432  nnge1  10557  halfpos  10765  lt2halves  10769  addltmul  10770  avglt2  10773  avgle2  10775  nnrecl  10789  zltlem1  10912  gtndiv  10936  nn01to3  11176  rebtwnz  11182  xrmax1  11379  max1ALT  11390  qbtwnre  11401  xralrple  11407  xltnegi  11418  xmulval  11427  xsubge0  11456  xposdif  11457  xlesubadd  11458  divelunit  11665  eluzgtdifelfzo  11859  fllelt  11915  flflp1  11925  flbi  11933  btwnzge0  11943  dfceil2  11950  ceilval2  11951  2submod  12030  om2uzlti  12043  monoord  12119  sermono  12121  expval  12150  expnbnd  12277  discr1  12284  discr  12285  facwordi  12349  seqcoll  12496  seqcoll2  12497  hashtpg  12507  swrdccat3blem  12711  cnpart  13155  sqrlem6  13163  sqrmo  13167  resqreu  13168  resqrtcl  13169  resqrtthlem  13170  sqrtneg  13183  sqreulem  13274  sqreu  13275  sqrtthlem  13277  eqsqrtd  13282  limsuple  13383  rlimcld2  13483  rlimrege0  13484  o1compt  13492  climserle  13567  caurcvgr  13578  fsum00  13694  fsumabs  13697  climcndslem2  13744  climcnds  13745  supcvg  13749  georeclim  13763  geoisumr  13769  cvgrat  13774  sin01bnd  14002  cos01bnd  14003  ruclem1  14048  ruclem9  14055  ruclem12  14058  dvdsaddr  14109  dvdssub  14110  dvdssubr  14111  dvdsfac  14125  dvdsmod  14127  oddp1even  14132  divalglem0  14135  divalglem2  14137  divalglem4  14138  divalglem5  14139  divalglem9  14143  divalg  14145  divalg2  14147  divalgmod  14148  ndvdssub  14149  ndvdsadd  14150  bitsfval  14157  bitsval  14158  bits0  14162  bitsp1  14165  bitsfzolem  14168  bitsfzo  14169  bitscmp  14172  bitsinv1lem  14175  bitsshft  14209  gcdcllem1  14233  dvdslegcd  14238  bezoutlem4  14263  dvdssqim  14275  dvdsmulgcd  14276  dvdssq  14282  nn0seqcvgd  14283  coprmdvds  14327  coprmdvds2  14328  isprm6  14334  prmdvdsexp  14339  prmdvdsexpr  14341  prmfac1  14343  divgcdodd  14344  rpmul  14348  hashdvds  14389  phiprmpw  14390  eulerthlem2  14396  prmdiv  14399  prmdiveq  14400  odzval  14402  odzcllem  14403  odzdvds  14406  opoe  14419  omoe  14420  pythagtriplem11  14433  pythagtriplem13  14435  pythagtrip  14442  pceulem  14453  pczndvds2  14474  pcdvdsb  14476  pc2dvds  14486  pcz  14488  pcprmpw2  14489  pcaddlem  14491  pcmpt  14495  prmpwdvds  14506  pockthlem  14507  prmreclem2  14519  prmreclem4  14521  4sqlem11  14557  vdwlem9  14591  rami  14617  ramlb  14621  0ram  14622  ramz2  14626  ramub1lem1  14628  imasleval  15030  subsubc  15341  pospo  15802  mulgval  16343  oddvdsnn0  16767  odmulg  16777  pgpfi1  16814  pgpfi  16824  slwispgp  16830  pgpssslw  16833  subgslw  16835  sylow2alem2  16837  sylow2blem3  16841  fislw  16844  efgi  16936  efgval2  16941  efgsrel  16951  efgredlemb  16963  lt6abl  17096  telgsums  17217  dprdval  17229  dprdvalOLD  17231  dprd2dlem2  17284  dprd2da  17286  dprd2d2  17288  ablfacrplem  17311  ablfac1a  17315  ablfac1b  17316  ablfac1eulem  17318  ablfac1eu  17319  pgpfac1lem3a  17322  ablfaclem3  17333  dvdsrtr  17496  dvdsrmul1  17497  unitpropd  17541  isabvd  17664  mplval  18279  ressmplbas2  18312  mplbaspropd  18473  zndvds0  18762  znunit  18775  cygth  18783  frlmup1  19000  lmisfree  19044  pmatcoe1fsupp  19369  fvmptnn04if  19517  hmphindis  20464  ordthmeolem  20468  psmettri2  20979  ismet2  21002  xmettri2  21009  imasdsf1olem  21042  imasf1oxmet  21044  comet  21182  stdbdxmet  21184  nmogelb  21389  nmolb  21390  metdsge  21519  metdseq0  21524  iihalf2  21599  bndth  21624  evth  21625  ipcau2  21843  tchcphlem1  21844  tchcphlem2  21845  iscau3  21883  iscmet3  21898  bcthlem1  21929  bcth  21934  minveclem3b  22009  minveclem3  22010  minveclem4  22013  minveclem5  22014  pjthlem1  22018  pjthlem2  22019  pmltpclem1  22026  pmltpc  22028  ivthlem2  22030  ivthlem3  22031  ovolgelb  22057  ovolunlem1  22074  ovoliunlem2  22080  ovolshftlem1  22086  ovolscalem1  22090  ovolicc1  22093  ovolicc2lem3  22096  ioombl1lem4  22137  mbfmulc2lem  22220  mbfposb  22226  mbfaddlem  22233  mbfsup  22237  mbfinf  22238  mbflimsup  22239  i1fposd  22280  itg1ge0a  22284  mbfi1fseqlem4  22291  mbfi1fseqlem6  22293  mbfi1flimlem  22295  mbfi1flim  22296  itg2const2  22314  itg2seq  22315  itg2monolem1  22323  itg2i1fseq  22328  itg2addlem  22331  ibllem  22337  isibl  22338  isibl2  22339  iblitg  22341  dfitg  22342  cbvitg  22348  itgeq2  22350  itgvallem  22357  iblneg  22375  itgneg  22376  itggt0  22414  dvlip  22560  c1lip1  22564  dvfsumle  22588  dvfsumlem2  22594  dvfsumlem4  22596  dvfsum2  22601  mdeglt  22631  degltp1le  22639  deg1suble  22674  ply1divex  22703  plypf1  22775  dgrlb  22799  coemulc  22818  dgrsub  22835  quotval  22854  plydivlem4  22858  quotcan  22871  vieta1lem2  22873  aalioulem2  22895  aaliou3lem9  22912  ulmcn  22960  dvradcnv  22982  sincosq1sgn  23057  sincosq2sgn  23058  sincosq4sgn  23060  logltb  23153  cxpge0  23232  cxple2  23246  logreclem  23301  jensen  23516  emcllem7  23529  wilthlem1  23540  ftalem2  23545  ftalem3  23546  ftalem7  23550  fta  23551  sgmval  23614  mumul  23653  dvdsppwf1o  23660  musum  23665  chtublem  23684  chtub  23685  perfect1  23701  bcmono  23750  bclbnd  23753  bposlem1  23757  bposlem5  23761  lgslem1  23769  lgsval  23773  lgsdilem  23795  lgsne0  23806  lgsqrlem2  23815  lgsqrlem4  23817  lgseisenlem1  23822  lgseisenlem2  23823  lgsquadlem1  23827  lgsquadlem2  23828  lgsquadlem3  23829  lgsquad2lem2  23832  m1lgs  23835  2sqlem4  23840  2sqlem8a  23844  2sqblem  23850  dchrisumlema  23871  dchrisumlem2  23873  dchrisumlem3  23874  chpdifbndlem2  23937  pntrsumbnd2  23950  pntpbnd1  23969  pntibndlem3  23975  pntlemi  23987  pntleme  23991  pntlem3  23992  pnt3  23995  ostth2lem2  24017  ostth3  24021  ostth  24022  tgcgrxfr  24110  islmib  24354  lmicom  24355  brbtwn2  24410  axlowdim2  24465  axlowdim  24466  axcontlem2  24470  axcontlem3  24471  axcontlem4  24472  axcontlem9  24477  axcontlem10  24478  axcontlem11  24479  axcontlem12  24480  ebtwntg  24487  ausisusgraedg  24558  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem2a  24987  nbhashuvtx1  25117  eupath2lem3  25181  eupath2  25182  konigsberg  25189  frgrareggt1  25318  ex-ind-dvds  25372  nmounbseqi  25890  nmounbseqiALT  25891  isblo3i  25914  blo3i  25915  blocnilem  25917  siilem2  25965  normlem6  26230  normgt0  26242  norm3dif  26265  norm3lemt  26267  pjhthlem1  26507  pjige0  26807  nmcexi  27143  lnconi  27150  lnopcnbd  27153  lnfncnbd  27174  riesz1  27182  cnlnadjlem2  27185  cnlnadjlem8  27191  leopg  27239  leop2  27241  leoppos  27243  leopadd  27249  leopmuli  27250  leopmul2i  27252  pjssge0i  27283  pjdifnormi  27284  pjssposi  27289  pjssdif1i  27292  chcv1  27472  cvexch  27491  atcvatlem  27502  atcvat3i  27513  atdmd  27515  cdj3i  27558  addltmulALT  27563  xrofsup  27816  xrge0addgt0  27915  omndadd  27930  omndmul2  27936  ogrpinvlt  27948  isinftm  27959  isarchi3  27965  archirng  27966  archirngz  27967  archiexdiv  27968  isorng  28024  orngmul  28028  ofldchr  28039  isarchiofld  28042  elrhmunit  28045  rearchi  28067  unitdivcld  28118  esumlub  28289  esumfsup  28299  esumcvg  28315  esum2d  28322  dya2ub  28478  omssubadd  28508  carsgmon  28522  itgeq12dv  28532  oddpwdc  28557  eulerpartlems  28563  prob01  28616  orvcval  28660  ballotlemfc0  28695  ballotlemfcc  28696  ballotleme  28699  ballotlem4  28701  ballotlem1c  28710  ballotlemsval  28711  ballotlemieq  28719  sgnmulsgp  28753  signsply0  28772  signslema  28783  signsvfpn  28806  lgamgulmlem1  28835  lgamgulmlem2  28836  lgamgulmlem3  28837  lgamgulmlem5  28839  lgambdd  28843  lgamcvglem  28846  erdszelem8  28906  erdsze2lem2  28912  abs2sqle  29310  abs2sqlt  29311  possumd  29357  pdivsq  29415  dvdspw  29416  poseq  29573  soseq  29574  sltval  29647  cgrdegen  29882  brofs  29883  segconeu  29889  btwntriv2  29890  transportprops  29912  brifs  29921  ifscgr  29922  brcgr3  29924  cgrxfr  29933  brcolinear2  29936  colineardim1  29939  brfs  29957  idinside  29962  btwnconn1lem11  29975  btwnconn1lem12  29976  btwnconn1lem14  29978  brsegle  29986  seglerflx  29990  seglemin  29991  segleantisym  29993  btwnsegle  29995  outsideofeu  30009  outsidele  30010  fvray  30019  ltflcei  30283  cos2h  30286  tan2h  30287  heicant  30289  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  dvtanlem  30304  itg2addnclem  30306  itg2addnclem2  30307  itg2gt0cn  30310  itggt0cn  30327  ftc1anclem5  30334  dvasin  30343  areacirclem1  30347  areacirclem4  30350  areacirclem5  30351  areacirc  30352  nn0prpwlem  30380  nn0prpw  30381  seqpo  30480  incsequz2  30482  mettrifi  30490  heibor1lem  30545  rrncmslem  30568  elpell1qr2  31047  monotuz  31116  monotoddzzfi  31117  monotoddzz  31118  oddcomabszz  31119  rmxypos  31124  mzpcong  31149  congrep  31150  acongsym  31153  acongneg2  31154  acongtr  31155  acongeq12d  31156  dvdsabsmod0  31167  divalgmodcl  31168  jm2.18  31169  jm2.19lem2  31171  jm2.19lem3  31172  jm2.19lem4  31173  jm2.19  31174  jm2.25  31180  jm2.15nn0  31184  jm2.16nn0  31185  jm2.27  31189  rmydioph  31195  expdiophlem1  31202  expdiophlem2  31203  fnwe2lem2  31236  dvgrat  31434  hashnzfz  31466  evth2f  31630  evthf  31642  rfcnpre3  31648  ltaddneg  31724  sublt0d  31734  upbdrech2  31747  fmul01  31813  fmul01lt1lem1  31817  climinf  31851  climinff  31856  limcrecl  31874  limsupre  31886  limclner  31896  cncficcgt0  31930  stoweidlem3  32024  stoweidlem7  32028  stoweidlem15  32036  stoweidlem16  32037  stoweidlem18  32039  stoweidlem26  32047  stoweidlem27  32048  stoweidlem28  32049  stoweidlem31  32052  stoweidlem34  32055  stoweidlem36  32057  stoweidlem37  32058  stoweidlem41  32062  stoweidlem44  32065  stoweidlem45  32066  stoweidlem46  32067  stoweidlem48  32069  stoweidlem51  32072  stoweidlem55  32076  stoweidlem59  32080  stoweidlem60  32081  stoweidlem62  32083  fourierdlem42  32170  fourierdlem50  32178  fourierdlem54  32182  fourierdlem68  32196  fourierdlem79  32207  fourierdlem96  32224  fourierdlem97  32225  fourierdlem98  32226  fourierdlem99  32227  fourierdlem105  32233  fourierdlem108  32236  fourierdlem110  32238  fourierdlem111  32239  etransclem24  32280  etransclem25  32281  etransclem35  32291  etransclem37  32293  etransclem41  32297  etransclem44  32300  bits0ALTV  32585  ltsubsubaddltsub  32698  subsubelfzo0  32712  nn0le2is012  33210  lcoop  33266  islininds  33301  ldepsnlinc  33363  ltsubaddb  33373  ltsubsubb  33374  ltsubadd2b  33375  logle1b  33408  loglt1b  33409  bigoval  33424  elbigo2r  33428  logbge0b  33438  logblt1b  33439  fldivexpfllog2  33440  nnlog2ge0lt1  33441  fllog2  33443  nnpw2pmod  33458  dignn0ldlem  33477  dig2nn1st  33480  lsatcv0eq  35169  oposlem  35304  oplecon1b  35323  opltcon1b  35327  atlatmstc  35441  cvlexch1  35450  cvlexch2  35451  cvlexchb2  35453  cvlatexchb2  35457  cvlatexch2  35459  cvlatcvr2  35464  cvlsupr2  35465  ishlat1  35474  hlsuprexch  35502  cvrexch  35541  cvrat  35543  atcvr0eq  35547  atcvrj0  35549  atltcvr  35556  cvrat3  35563  cvrat4  35564  cvrat42  35565  3noncolr2  35570  hlatcon2  35573  4noncolr3  35574  3dimlem1  35579  3dimlem2  35580  3dimlem3a  35581  3dimlem3  35582  3dimlem3OLDN  35583  3dimlem4a  35584  3dimlem4  35585  3dimlem4OLDN  35586  3dim1lem5  35587  3dim2  35589  3dim3  35590  ps-1  35598  ps-2  35599  3atlem5  35608  3atlem6  35609  lplni2  35658  lplnnle2at  35662  lplnnleat  35663  lplnnlelln  35664  lplnribN  35672  lplnexllnN  35685  lvoli2  35702  lvolnle3at  35703  lvolnleat  35704  lvolnlelln  35705  lvolnlelpln  35706  4atlem9  35724  4atlem10a  35725  4atlem11a  35728  4atlem11  35730  4atlem12a  35731  dalempnes  35772  dalemqnet  35773  dalem1  35780  dalemswapyzps  35811  dalemrotps  35812  dalem30  35823  dalem35  35828  lineset  35859  islinei  35861  psubspset  35865  psubspi2N  35869  snatpsubN  35871  2llnma1  35908  elpaddn0  35921  elpaddri  35923  elpaddat  35925  elpadd2at  35927  paddcom  35934  paddasslem12  35952  pmapjat1  35974  llnexchb2  35990  lhp2at0nle  36156  lhprelat3N  36161  4atexlemswapqr  36184  4atexlemcnd  36193  lautle  36205  lautcvr  36213  ltrnel  36260  ltrneq2  36269  trlnle  36308  cdlemc3  36315  cdlemd6  36325  cdleme3  36359  cdleme7aa  36364  cdleme7  36371  cdleme11c  36383  cdleme15c  36398  cdleme20yOLD  36425  cdleme20m  36446  cdleme21b  36449  cdleme21c  36450  cdleme21at  36451  cdleme36a  36583  cdleme43bN  36613  cdleme43dN  36615  cdleme46f2g2  36616  cdleme46f2g1  36617  cdlemeg46c  36636  cdlemeg46nlpq  36640  cdlemb3  36729  cdlemg4d  36736  cdlemg6d  36744  cdlemg10c  36762  cdlemg12  36773  cdlemg27b  36819  djhcvat42  37539  relexpxpmin  38226  relexpmulg  38228  inductionexd  38419  leeq2d  38422  imo72b2lem0  38434  imo72b2lem2  38436  imo72b2lem1  38440  imo72b2  38445
  Copyright terms: Public domain W3C validator