MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq1 Structured version   Visualization version   GIF version

Theorem neeq1 3073
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
Assertion
Ref Expression
neeq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neeq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21neeq1d 3070 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wne 3011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815  df-ne 3012
This theorem is referenced by:  pm13.18  3092  nelrdva  3671  psseq1  4039  n0snor2el  4737  0inp0  5236  nnullss  5331  opeqex  5365  fri  5494  frsn  5616  xp11  6010  limeq  6181  tz6.12i  6678  fveqressseq  6829  funopsn  6892  fprg  6899  tpres  6945  f1dom3el3dif  7010  f1prex  7023  isofrlem  7077  f1oweALT  7659  frxp  7807  suppimacnv  7828  elqsn0  8353  frfi  8751  fiint  8783  marypha1lem  8885  eldju2ndl  9341  dfac8alem  9444  dfac8clem  9447  aceq3lem  9535  dfac5lem3  9540  dfac5lem4  9541  dfac5  9543  dfac2b  9545  dfac9  9551  kmlem1  9565  kmlem12  9576  kmlem14  9578  fin2i  9706  isfin2-2  9730  fin23lem21  9750  fin1a2lem10  9820  axcc2lem  9847  dominf  9856  ac5b  9889  zornn0g  9916  axdclem  9930  dominfac  9984  elwina  10097  elina  10098  iswun  10115  rankcf  10188  axrrecex  10574  elimne0  10620  1re  10630  recex  11261  xnn0nemnf  11966  uzn0  12248  qreccl  12356  xrnemnf  12500  xrnepnf  12501  xnn0n0n1ge2b  12514  fztpval  12964  expcl2lem  13437  hashnemnf  13700  hashneq0  13721  hashge2el2difr  13835  hashdmpropge2  13837  relexp1g  14376  ntrivcvgn0  15245  ntrivcvgmullem  15248  fprodntriv  15287  divalglem7  15739  divalg  15743  gcdcllem1  15837  gcdcllem3  15839  pcpre1  16168  pcqmul  16179  pcqcl  16182  prmgaplem3  16378  prmgaplem4  16379  xpsfrnel  16826  mreintcl  16857  isdrs  17535  isipodrs  17762  sgrp2rid2ex  18083  frgpuptinv  18888  isdrngrd  19519  isnzr2  20027  psgnodpmr  20277  lindfrn  20508  dmatelnd  21099  dmatmul  21100  mdetdiaglem  21201  mdetunilem1  21215  fvmptnn04ifa  21453  chfacfscmulgsum  21463  chfacfpmmulgsum  21467  fiinopn  21504  hausnei  21931  dfconn2  22022  2ndcdisj  22059  regr1lem2  22343  isfbas  22432  ioorinv  24178  ioorcl  24179  vitalilem2  24211  vitalilem3  24212  vitali  24215  itg1climres  24316  mbfi1fseqlem4  24320  dvferm1lem  24585  dvferm2lem  24587  isuc1p  24739  ismon1p  24741  ply1remlem  24761  plydivlem4  24890  aannenlem1  24922  aannenlem2  24923  lgsne0  25917  lgsqr  25933  axtg5seg  26257  axtgupdim2  26263  axtgeucl  26264  axlowdim1  26751  lpvtx  26859  umgrnloopv  26897  usgrnloopvALT  26989  umgrvad2edg  27001  cusgrfilem2  27244  pthdlem2lem  27554  iswwlks  27620  iswwlksnx  27624  2pthdlem1  27714  isclwwlk  27767  3pthdlem1  27947  upgr3v3e3cycl  27963  upgr4cycl4dv4e  27968  eupth2lem2  28002  eupth2lem3lem4  28014  eupth2lem3lem6  28016  3cyclfrgrrn1  28068  4cycl2vnunb  28073  frgrreg  28177  norm1exi  29031  shintcl  29111  chintcl  29113  chne0  29275  elspansn2  29348  eigre  29616  eigorth  29619  kbpj  29737  superpos  30135  hatomic  30141  isprmidl  30995  ismxidl  31013  ssmxidllem  31020  ssmxidl  31021  xrge0iifhom  31254  xrge0iif1  31255  esumpr2  31400  sibfof  31672  signswn0  31904  signswch  31905  signstfvneq0  31916  axtgupdim2ALTV  32013  bnj168  32074  bnj970  32293  bnj1154  32345  umgracycusgr  32475  cusgracyclt3v  32477  subfacp1lem1  32500  erdszelem8  32519  indispconn  32555  cvmsss2  32595  nepss  33022  frmin  33158  elwlim  33184  nolesgn2ores  33253  nosepdmlem  33261  nosupbnd1lem3  33284  nosupbnd1lem5  33286  nosupbnd2lem1  33289  dfrdg4  33486  fvray  33676  linedegen  33678  fvline  33679  hilbert1.1  33689  rankeq1o  33706  unblimceq0lem  33919  knoppndvlem21  33945  poimirlem1  35016  poimirlem17  35032  poimirlem20  35035  poimirlem32  35047  itg2addnclem3  35068  neificl  35149  isdrngo3  35355  ispridl  35430  ismaxidl  35436  islshp  36233  lsatn0  36253  lshpset2N  36373  atlex  36570  hlsuprexch  36635  3dimlem1  36712  llni2  36766  lplni2  36791  2llnjN  36821  lvoli2  36835  2lplnj  36874  islinei  36994  lnatexN  37033  llnexchb2  37123  lhpmatb  37285  cdleme40m  37721  cdlemftr3  37819  cdlemk28-3  38162  cdlemk35s  38191  cdlemk39s  38193  cdlemk42  38195  nnn1suc  39411  dnnumch1  39918  aomclem3  39930  aomclem8  39935  dfac11  39936  dfacbasgrp  39982  dfsucon  40161  ax6e2ndeq  41199  ax6e2ndeqVD  41549  fnchoice  41592  fiiuncl  41633  disjrnmpt2  41753  idlimc  42207  limcperiod  42209  limclner  42232  cnrefiisp  42411  climxlim2lem  42426  fperdvper  42500  stoweidlem35  42616  stoweidlem43  42624  stoweidlem59  42640  fourierdlem76  42763  etransclem47  42862  nnfoctbdjlem  43033  elprneb  43560  ichexmpl1  43925  ichnreuop  43928  nrhmzr  44436  itcoval2  45017  itcoval3  45018  itcovalsuc  45020  ackvalsuc1mpt  45031  inlinecirc02plem  45139
  Copyright terms: Public domain W3C validator