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

Theorem neleq1 3051
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 3050 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wnel 3046
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 3047
This theorem is referenced by:  ruALT  9544  ssnn0fi  13896  cnpart  15131  sqrmo  15142  resqrtcl  15144  resqrtthlem  15145  sqrtneg  15158  sqreu  15251  sqrtthlem  15253  eqsqrtd  15258  ge2nprmge4  16582  prmgaplem7  16934  mgmnsgrpex  18746  sgrpnmndex  18747  iccpnfcnv  24323  griedg0prc  28254  nbgrssovtx  28351  rgrusgrprc  28579  rusgrprc  28580  rgrprcx  28582  frgrwopreglem4a  29296  xrge0iifcnv  32571  0nn0m1nnn0  33760  fpprel  46006  oddinmgm  46195
  Copyright terms: Public domain W3C validator