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

Theorem breq2d 4464
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1d.1
Assertion
Ref Expression
breq2d

Proof of Theorem breq2d
StepHypRef Expression
1 breq1d.1 . 2
2 breq2 4456 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  breqtrd  4476  sbcbr1g  4507  pofun  4821  csbfv12  5906  csbfv12gOLD  5907  isorel  6222  soisores  6223  soisoi  6224  isocnv  6226  isotr  6232  f1owe  6249  caovordig  6480  caovordg  6482  caovord  6486  f1oweALT  6784  frxp  6910  xporderlem  6911  fnwelem  6915  difsnen  7619  domdifsn  7620  unfilem3  7806  domunfican  7813  marypha1lem  7913  marypha1  7914  wemapwe  8160  oef1o  8162  r1sdom  8213  sdomsdomcardi  8373  alephordi  8476  pwcdadom  8617  sornom  8678  axdclem  8920  pwcfsdom  8979  elgch  9021  winalim2  9095  rankcf  9176  inatsk  9177  pinq  9326  nqereu  9328  ltaddnq  9373  ltrnq  9378  archnq  9379  addclprlem1  9415  mulclprlem  9418  1idpr  9428  ltaprlem  9443  ltapr  9444  prlem936  9446  ltasr  9498  mulgt0sr  9503  sqgt0sr  9504  map2psrpr  9508  axpre-ltadd  9565  axpre-mulgt0  9566  axpre-sup  9567  ltsubadd2  10048  lesubadd2  10050  ltaddpos2  10068  posdif  10070  lesub1  10071  ltnegcon1  10078  lenegcon1  10081  addge02  10088  leaddle0  10092  mulge0  10095  msqge0  10099  ltordlem  10103  prodgt0  10412  prodgt02  10413  prodge02  10415  ltmulgt12  10428  lemulge12  10430  mulge0b  10437  mulle0b  10438  ltdivmul  10442  ledivmul  10443  ledivmulOLD  10444  ltdivmul2  10445  lt2mul2div  10446  ledivmul2  10447  ledivmul2OLD  10448  ltrec  10451  ltrec1  10457  ltdiv23  10461  lediv23  10462  nnge1  10587  halfpos  10794  lt2halves  10798  addltmul  10799  avglt2  10802  avgle2  10804  nnrecl  10818  zltlem1  10941  gtndiv  10965  nn01to3  11204  rebtwnz  11210  xrmax1  11405  max1ALT  11416  qbtwnre  11427  xralrple  11433  xltnegi  11444  xmulval  11453  xsubge0  11482  xposdif  11483  xlesubadd  11484  divelunit  11691  eluzgtdifelfzo  11878  fllelt  11934  flflp1  11944  flbi  11952  btwnzge0  11961  dfceil2  11968  ceilval2  11969  2submod  12048  om2uzlti  12061  monoord  12137  sermono  12139  expval  12168  expnbnd  12295  discr1  12302  discr  12303  facwordi  12367  seqcoll  12512  seqcoll2  12513  hashtpg  12523  swrdccat3blem  12720  cnpart  13073  sqrlem6  13081  sqrmo  13085  resqreu  13086  resqrtcl  13087  resqrtthlem  13088  sqrtneg  13101  sqreulem  13192  sqreu  13193  sqrtthlem  13195  eqsqrtd  13200  limsuple  13301  rlimcld2  13401  rlimrege0  13402  o1compt  13410  climserle  13485  caurcvgr  13496  fsum00  13612  fsumabs  13615  climcndslem2  13662  climcnds  13663  supcvg  13667  georeclim  13681  geoisumr  13687  cvgrat  13692  sin01bnd  13920  cos01bnd  13921  ruclem1  13964  ruclem9  13971  ruclem12  13974  dvdsaddr  14025  dvdssub  14026  dvdssubr  14027  dvdsfac  14041  dvdsmod  14043  oddp1even  14048  divalglem0  14051  divalglem2  14053  divalglem4  14054  divalglem5  14055  divalglem9  14059  divalg  14061  divalg2  14063  divalgmod  14064  ndvdssub  14065  ndvdsadd  14066  bitsfval  14073  bitsval  14074  bits0  14078  bitsp1  14081  bitsfzolem  14084  bitsfzo  14085  bitscmp  14088  bitsinv1lem  14091  bitsshft  14125  gcdcllem1  14149  dvdslegcd  14154  bezoutlem4  14179  dvdssqim  14191  dvdsmulgcd  14192  dvdssq  14198  nn0seqcvgd  14199  coprmdvds  14243  coprmdvds2  14244  isprm6  14250  prmdvdsexp  14255  prmdvdsexpr  14257  prmfac1  14259  divgcdodd  14260  rpmul  14264  hashdvds  14305  phiprmpw  14306  eulerthlem2  14312  prmdiv  14315  prmdiveq  14316  odzval  14318  odzcllem  14319  odzdvds  14322  opoe  14335  omoe  14336  pythagtriplem11  14349  pythagtriplem13  14351  pythagtrip  14358  pceulem  14369  pczndvds2  14390  pcdvdsb  14392  pc2dvds  14402  pcz  14404  pcprmpw2  14405  pcaddlem  14407  pcmpt  14411  prmpwdvds  14422  pockthlem  14423  prmreclem2  14435  prmreclem4  14437  4sqlem11  14473  vdwlem9  14507  rami  14533  ramlb  14537  0ram  14538  ramz2  14542  ramub1lem1  14544  imasleval  14938  subsubc  15222  pospo  15603  mulgval  16144  oddvdsnn0  16568  odmulg  16578  pgpfi1  16615  pgpfi  16625  slwispgp  16631  pgpssslw  16634  subgslw  16636  sylow2alem2  16638  sylow2blem3  16642  fislw  16645  efgi  16737  efgval2  16742  efgsrel  16752  efgredlemb  16764  lt6abl  16897  telgsums  17022  dprdval  17034  dprdvalOLD  17036  dprd2dlem2  17089  dprd2da  17091  dprd2d2  17093  ablfacrplem  17116  ablfac1a  17120  ablfac1b  17121  ablfac1eulem  17123  ablfac1eu  17124  pgpfac1lem3a  17127  ablfaclem3  17138  dvdsrtr  17301  dvdsrmul1  17302  unitpropd  17346  isabvd  17469  mplval  18084  ressmplbas2  18117  mplbaspropd  18278  zndvds0  18589  znunit  18602  cygth  18610  frlmup1  18832  lmisfree  18877  pmatcoe1fsupp  19202  fvmptnn04if  19350  hmphindis  20298  ordthmeolem  20302  psmettri2  20813  ismet2  20836  xmettri2  20843  imasdsf1olem  20876  imasf1oxmet  20878  comet  21016  stdbdxmet  21018  nmogelb  21223  nmolb  21224  metdsge  21353  metdseq0  21358  iihalf2  21433  bndth  21458  evth  21459  ipcau2  21677  tchcphlem1  21678  tchcphlem2  21679  iscau3  21717  iscmet3  21732  bcthlem1  21763  bcth  21768  minveclem3b  21843  minveclem3  21844  minveclem4  21847  minveclem5  21848  pjthlem1  21852  pjthlem2  21853  pmltpclem1  21860  pmltpc  21862  ivthlem2  21864  ivthlem3  21865  ovolgelb  21891  ovolunlem1  21908  ovoliunlem2  21914  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem3  21930  ioombl1lem4  21971  mbfmulc2lem  22054  mbfposb  22060  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  mbflimsup  22073  i1fposd  22114  itg1ge0a  22118  mbfi1fseqlem4  22125  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfi1flim  22130  itg2const2  22148  itg2seq  22149  itg2monolem1  22157  itg2i1fseq  22162  itg2addlem  22165  ibllem  22171  isibl  22172  isibl2  22173  iblitg  22175  dfitg  22176  cbvitg  22182  itgeq2  22184  itgvallem  22191  iblneg  22209  itgneg  22210  itggt0  22248  dvlip  22394  c1lip1  22398  dvfsumle  22422  dvfsumlem2  22428  dvfsumlem4  22430  dvfsum2  22435  mdeglt  22465  degltp1le  22473  deg1suble  22508  ply1divex  22537  plypf1  22609  dgrlb  22633  coemulc  22652  dgrsub  22669  quotval  22688  plydivlem4  22692  quotcan  22705  vieta1lem2  22707  aalioulem2  22729  aaliou3lem9  22746  ulmcn  22794  dvradcnv  22816  sincosq1sgn  22891  sincosq2sgn  22892  sincosq4sgn  22894  logltb  22984  cxpge0  23064  cxple2  23078  logreclem  23150  jensen  23318  emcllem7  23331  wilthlem1  23342  ftalem2  23347  ftalem3  23348  ftalem7  23352  fta  23353  sgmval  23416  mumul  23455  dvdsppwf1o  23462  musum  23467  chtublem  23486  chtub  23487  perfect1  23503  bcmono  23552  bclbnd  23555  bposlem1  23559  bposlem5  23563  lgslem1  23571  lgsval  23575  lgsdilem  23597  lgsne0  23608  lgsqrlem2  23617  lgsqrlem4  23619  lgseisenlem1  23624  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  lgsquad2lem2  23634  m1lgs  23637  2sqlem4  23642  2sqlem8a  23646  2sqblem  23652  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  chpdifbndlem2  23739  pntrsumbnd2  23752  pntpbnd1  23771  pntibndlem3  23777  pntlemi  23789  pntleme  23793  pntlem3  23794  pnt3  23797  ostth2lem2  23819  ostth3  23823  ostth  23824  tgcgrxfr  23909  islmib  24153  lmicom  24154  brbtwn2  24208  axlowdim2  24263  axlowdim  24264  axcontlem2  24268  axcontlem3  24269  axcontlem4  24270  axcontlem9  24275  axcontlem10  24276  axcontlem11  24277  axcontlem12  24278  ebtwntg  24285  ausisusgraedg  24356  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  nbhashuvtx1  24915  eupath2lem3  24979  eupath2  24980  konigsberg  24987  frgrareggt1  25116  ex-ind-dvds  25170  nmounbseqi  25692  nmounbseqiOLD  25693  isblo3i  25716  blo3i  25717  blocnilem  25719  siilem2  25767  normlem6  26032  normgt0  26044  norm3dif  26067  norm3lemt  26069  pjhthlem1  26309  pjige0  26609  nmcexi  26945  lnconi  26952  lnopcnbd  26955  lnfncnbd  26976  riesz1  26984  cnlnadjlem2  26987  cnlnadjlem8  26993  leopg  27041  leop2  27043  leoppos  27045  leopadd  27051  leopmuli  27052  leopmul2i  27054  pjssge0i  27085  pjdifnormi  27086  pjssposi  27091  pjssdif1i  27094  chcv1  27274  cvexch  27293  atcvatlem  27304  atcvat3i  27315  atdmd  27317  cdj3i  27360  addltmulALT  27365  xrofsup  27582  xrge0addgt0  27681  omndadd  27696  omndmul2  27702  ogrpinvlt  27714  isinftm  27725  isarchi3  27731  archirng  27732  archirngz  27733  archiexdiv  27734  isorng  27789  orngmul  27793  ofldchr  27804  isarchiofld  27807  elrhmunit  27810  rearchi  27832  unitdivcld  27883  esumlub  28068  esumfsup  28076  esumcvg  28092  dya2ub  28241  itgeq12dv  28268  oddpwdc  28293  eulerpartlems  28299  prob01  28352  orvcval  28396  ballotlemfc0  28431  ballotlemfcc  28432  ballotleme  28435  ballotlem4  28437  ballotlem1c  28446  ballotlemsval  28447  ballotlemieq  28455  sgnmulsgp  28489  signsply0  28508  signslema  28519  signsvfpn  28542  lgamgulmlem1  28571  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgambdd  28579  lgamcvglem  28582  erdszelem8  28642  erdsze2lem2  28648  abs2sqle  29046  abs2sqlt  29047  possumd  29116  pdivsq  29174  dvdspw  29175  poseq  29333  soseq  29334  sltval  29407  cgrdegen  29654  brofs  29655  segconeu  29661  btwntriv2  29662  transportprops  29684  brifs  29693  ifscgr  29694  brcgr3  29696  cgrxfr  29705  brcolinear2  29708  colineardim1  29711  brfs  29729  idinside  29734  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem14  29750  brsegle  29758  seglerflx  29762  seglemin  29763  segleantisym  29765  btwnsegle  29767  outsideofeu  29781  outsidele  29782  fvray  29791  ltflcei  30043  cos2h  30046  tan2h  30047  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  itg2gt0cn  30070  itggt0cn  30087  ftc1anclem5  30094  dvasin  30103  areacirclem1  30107  areacirclem4  30110  areacirclem5  30111  areacirc  30112  nn0prpwlem  30140  nn0prpw  30141  seqpo  30240  incsequz2  30242  mettrifi  30250  heibor1lem  30305  rrncmslem  30328  elpell1qr2  30808  monotuz  30877  monotoddzzfi  30878  monotoddzz  30879  oddcomabszz  30880  rmxypos  30885  mzpcong  30910  congrep  30911  acongsym  30914  acongneg2  30915  acongtr  30916  acongeq12d  30917  dvdsabsmod0  30928  divalgmodcl  30929  jm2.18  30930  jm2.19lem2  30932  jm2.19lem3  30933  jm2.19lem4  30934  jm2.19  30935  jm2.25  30941  jm2.15nn0  30945  jm2.16nn0  30946  jm2.27  30950  rmydioph  30956  expdiophlem1  30963  expdiophlem2  30964  fnwe2lem2  30997  dvgrat  31193  hashnzfz  31225  evth2f  31390  evthf  31402  rfcnpre3  31408  ltaddneg  31484  sublt0d  31495  upbdrech2  31508  fmul01  31574  fmul01lt1lem1  31578  climinf  31612  climinff  31617  limcrecl  31635  limsupre  31647  limclner  31657  cncficcgt0  31691  stoweidlem3  31785  stoweidlem7  31789  stoweidlem15  31797  stoweidlem16  31798  stoweidlem18  31800  stoweidlem26  31808  stoweidlem27  31809  stoweidlem28  31810  stoweidlem31  31813  stoweidlem34  31816  stoweidlem36  31818  stoweidlem37  31819  stoweidlem41  31823  stoweidlem44  31826  stoweidlem45  31827  stoweidlem46  31828  stoweidlem48  31830  stoweidlem51  31833  stoweidlem55  31837  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  fourierdlem42  31931  fourierdlem50  31939  fourierdlem54  31943  fourierdlem68  31957  fourierdlem79  31968  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem105  31994  fourierdlem108  31997  fourierdlem110  31999  fourierdlem111  32000  etransclem24  32041  etransclem25  32042  etransclem35  32052  etransclem37  32054  etransclem41  32058  etransclem44  32061  ltsubsubaddltsub  32324  subsubelfzo0  32338  nn0le2is012  32956  lcoop  33012  islininds  33047  ldepsnlinc  33109  lsatcv0eq  34772  oposlem  34907  oplecon1b  34926  opltcon1b  34930  atlatmstc  35044  cvlexch1  35053  cvlexch2  35054  cvlexchb2  35056  cvlatexchb2  35060  cvlatexch2  35062  cvlatcvr2  35067  cvlsupr2  35068  ishlat1  35077  hlsuprexch  35105  cvrexch  35144  cvrat  35146  atcvr0eq  35150  atcvrj0  35152  atltcvr  35159  cvrat3  35166  cvrat4  35167  cvrat42  35168  3noncolr2  35173  hlatcon2  35176  4noncolr3  35177  3dimlem1  35182  3dimlem2  35183  3dimlem3a  35184  3dimlem3  35185  3dimlem3OLDN  35186  3dimlem4a  35187  3dimlem4  35188  3dimlem4OLDN  35189  3dim1lem5  35190  3dim2  35192  3dim3  35193  ps-1  35201  ps-2  35202  3atlem5  35211  3atlem6  35212  lplni2  35261  lplnnle2at  35265  lplnnleat  35266  lplnnlelln  35267  lplnribN  35275  lplnexllnN  35288  lvoli2  35305  lvolnle3at  35306  lvolnleat  35307  lvolnlelln  35308  lvolnlelpln  35309  4atlem9  35327  4atlem10a  35328  4atlem11a  35331  4atlem11  35333  4atlem12a  35334  dalempnes  35375  dalemqnet  35376  dalem1  35383  dalemswapyzps  35414  dalemrotps  35415  dalem30  35426  dalem35  35431  lineset  35462  islinei  35464  psubspset  35468  psubspi2N  35472  snatpsubN  35474  2llnma1  35511  elpaddn0  35524  elpaddri  35526  elpaddat  35528  elpadd2at  35530  paddcom  35537  paddasslem12  35555  pmapjat1  35577  llnexchb2  35593  lhp2at0nle  35759  lhprelat3N  35764  4atexlemswapqr  35787  4atexlemcnd  35796  lautle  35808  lautcvr  35816  ltrnel  35863  ltrneq2  35872  trlnle  35911  cdlemc3  35918  cdlemd6  35928  cdleme3  35962  cdleme7aa  35967  cdleme7  35974  cdleme11c  35986  cdleme15c  36001  cdleme20yOLD  36028  cdleme20m  36049  cdleme21b  36052  cdleme21c  36053  cdleme21at  36054  cdleme36a  36186  cdleme43bN  36216  cdleme43dN  36218  cdleme46f2g2  36219  cdleme46f2g1  36220  cdlemeg46c  36239  cdlemeg46nlpq  36243  cdlemb3  36332  cdlemg4d  36339  cdlemg6d  36347  cdlemg10c  36365  cdlemg12  36376  cdlemg27b  36422  djhcvat42  37142  inductionexd  37967  leeq2d  37970  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator