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

Theorem neleq1 3053
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 2734 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3052 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wnel 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-nel 3048
This theorem is referenced by:  ruALT  9598  ssnn0fi  13950  cnpart  15187  sqrmo  15198  resqrtcl  15200  resqrtthlem  15201  sqrtneg  15214  sqreu  15307  sqrtthlem  15309  eqsqrtd  15314  ge2nprmge4  16638  prmgaplem7  16990  mgmnsgrpex  18812  sgrpnmndex  18813  iccpnfcnv  24460  griedg0prc  28552  nbgrssovtx  28649  rgrusgrprc  28877  rusgrprc  28878  rgrprcx  28880  frgrwopreglem4a  29594  xrge0iifcnv  32944  0nn0m1nnn0  34133  fpprel  46444  oddinmgm  46633
  Copyright terms: Public domain W3C validator