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

Theorem neleq1 3052
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 2738 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3051 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wnel 3046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-nel 3047
This theorem is referenced by:  ruALT  9643  ssnn0fi  14026  cnpart  15279  sqrmo  15290  resqrtcl  15292  resqrtthlem  15293  sqrtneg  15306  sqreu  15399  sqrtthlem  15401  eqsqrtd  15406  ge2nprmge4  16738  prmgaplem7  17095  mgmnsgrpex  18944  sgrpnmndex  18945  iccpnfcnv  24975  griedg0prc  29281  nbgrssovtx  29378  rgrusgrprc  29607  rusgrprc  29608  rgrprcx  29610  frgrwopreglem4a  30329  xrge0iifcnv  33932  0nn0m1nnn0  35118  fpprel  47715  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  oddinmgm  48091
  Copyright terms: Public domain W3C validator