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

Theorem neeq1 3047
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 3044 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wne 2985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2806  df-ne 2986
This theorem is referenced by:  nelrdva  3622  psseq1  3899  ssdifsnOLD  4517  n0snor2el  4559  0inp0  5036  nnullss  5127  opeqex  5158  fri  5280  frsn  5398  xp11  5787  limeq  5955  tz6.12i  6437  fveqressseq  6580  funopsn  6640  fprg  6649  tpres  6694  f1dom3el3dif  6753  f1prex  6766  isofrlem  6817  f1oweALT  7385  frxp  7524  suppimacnv  7543  elqsn0  8054  frfi  8447  fiint  8479  marypha1lem  8581  eldju2ndl  9036  dfac8alem  9138  dfac8clem  9141  aceq3lem  9229  dfac5lem3  9234  dfac5lem4  9235  dfac5  9237  dfac2b  9239  dfac2OLD  9241  dfac9  9246  kmlem1  9260  kmlem12  9271  kmlem14  9273  fin2i  9405  isfin2-2  9429  fin23lem21  9449  fin1a2lem10  9519  axcc2lem  9546  dominf  9555  ac5b  9588  zornn0g  9615  axdclem  9629  dominfac  9683  elwina  9796  elina  9797  iswun  9814  rankcf  9887  axrrecex  10272  elimne0  10318  1re  10328  recex  10947  xnn0nemnf  11643  uzn0  11923  qreccl  12030  xrnemnf  12170  xrnepnf  12171  xnn0n0n1ge2b  12184  fztpval  12628  expcl2lem  13098  hashnemnf  13355  hashneq0  13376  hashge2el2difr  13483  hashdmpropge2  13485  relexp1g  13992  ntrivcvgn0  14854  ntrivcvgmullem  14857  fprodntriv  14896  divalglem7  15345  divalg  15349  gcdcllem1  15443  gcdcllem3  15445  pcpre1  15767  pcqmul  15778  pcqcl  15781  prmgaplem3  15977  prmgaplem4  15978  xpscfv  16430  xpsfrnel  16431  mreintcl  16463  isdrs  17142  isipodrs  17369  sgrp2rid2ex  17622  frgpuptinv  18388  isdrngrd  18980  isnzr2  19475  psgnodpmr  20146  lindfrn  20374  dmatelnd  20517  dmatmul  20518  mdetdiaglem  20619  mdetunilem1  20633  fvmptnn04ifa  20872  chfacfscmulgsum  20882  chfacfpmmulgsum  20886  fiinopn  20923  hausnei  21350  dfconn2  21440  2ndcdisj  21477  regr1lem2  21761  isfbas  21850  ioorinv  23563  ioorcl  23564  vitalilem2  23596  vitalilem3  23597  vitali  23600  itg1climres  23701  mbfi1fseqlem4  23705  dvferm1lem  23967  dvferm2lem  23969  isuc1p  24120  ismon1p  24122  ply1remlem  24142  plydivlem4  24271  aannenlem1  24303  aannenlem2  24304  lgsne0  25280  lgsqr  25296  axtg5seg  25584  axtgupdim2  25590  axtgeucl  25591  axlowdim1  26059  structgrssvtxlemOLD  26135  lpvtx  26183  umgrnloopv  26221  usgrnloopvALT  26314  umgrvad2edg  26326  cusgrfilem2  26586  pthdlem2lem  26897  iswwlks  26963  iswwlksnx  26967  2pthdlem1  27076  isclwwlk  27133  3pthdlem1  27343  upgr3v3e3cycl  27359  upgr4cycl4dv4e  27364  eupth2lem2  27398  eupth2lem3lem4  27410  eupth2lem3lem6  27412  3cyclfrgrrn1  27466  4cycl2vnunb  27471  frgrreg  27588  norm1exi  28441  shintcl  28523  chintcl  28525  chne0  28687  elspansn2  28760  eigre  29028  eigorth  29031  kbpj  29149  superpos  29547  hatomic  29553  xrge0iifhom  30314  xrge0iif1  30315  esumpr2  30460  sibfof  30733  signswn0  30968  signswch  30969  signstfvneq0  30980  axtgupdim2OLD  31077  bnj168  31127  bnj970  31345  bnj1154  31395  subfacp1lem1  31489  erdszelem8  31508  indispconn  31544  cvmsss2  31584  nepss  31926  frmin  32068  elwlim  32094  nolesgn2ores  32151  nosepdmlem  32159  nosupbnd1lem3  32182  nosupbnd1lem5  32184  nosupbnd2lem1  32187  dfrdg4  32384  fvray  32574  linedegen  32576  fvline  32577  hilbert1.1  32587  rankeq1o  32604  unblimceq0lem  32819  knoppndvlem21  32845  poimirlem1  33725  poimirlem17  33741  poimirlem20  33744  poimirlem32  33756  itg2addnclem3  33777  neificl  33862  isdrngo3  34071  ispridl  34146  ismaxidl  34152  islshp  34761  lsatn0  34781  lshpset2N  34901  atlex  35098  hlsuprexch  35163  3dimlem1  35240  llni2  35294  lplni2  35319  2llnjN  35349  lvoli2  35363  2lplnj  35402  islinei  35522  lnatexN  35561  llnexchb2  35651  lhpmatb  35813  cdleme40m  36249  cdlemftr3  36347  cdlemk28-3  36690  cdlemk35s  36719  cdlemk39s  36721  cdlemk42  36723  dnnumch1  38116  aomclem3  38128  aomclem8  38133  dfac11  38134  dfacbasgrp  38180  ax6e2ndeq  39274  ax6e2ndeqVD  39640  fnchoice  39683  fiiuncl  39728  disjrnmpt2  39865  idlimc  40339  limcperiod  40341  limclner  40364  cnrefiisp  40537  climxlim2lem  40552  fperdvper  40614  stoweidlem35  40732  stoweidlem43  40740  stoweidlem59  40756  fourierdlem76  40879  etransclem47  40978  nnfoctbdjlem  41152  elprneb  41654  nrhmzr  42442
  Copyright terms: Public domain W3C validator