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

Theorem neleq1 3042
Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Assertion
Ref Expression
neleq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neleq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
2 eqidd 2727 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3041 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  wnel 3036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803  df-nel 3037
This theorem is referenced by:  ruALT  9646  ssnn0fi  14005  cnpart  15245  sqrmo  15256  resqrtcl  15258  resqrtthlem  15259  sqrtneg  15272  sqreu  15365  sqrtthlem  15367  eqsqrtd  15372  ge2nprmge4  16702  prmgaplem7  17059  mgmnsgrpex  18921  sgrpnmndex  18922  iccpnfcnv  24960  griedg0prc  29200  nbgrssovtx  29297  rgrusgrprc  29526  rusgrprc  29527  rgrprcx  29529  frgrwopreglem4a  30243  xrge0iifcnv  33748  0nn0m1nnn0  34940  fpprel  47300  oddinmgm  47552
  Copyright terms: Public domain W3C validator