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

Theorem neleq1 3097
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 2798 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3096 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1525  wnel 3092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-clel 2865  df-nel 3093
This theorem is referenced by:  ruALT  8920  ssnn0fi  13207  cnpart  14437  sqrmo  14449  resqrtcl  14451  resqrtthlem  14452  sqrtneg  14465  sqreu  14558  sqrtthlem  14560  eqsqrtd  14565  ge2nprmge4  15878  prmgaplem7  16226  mgmnsgrpex  17861  sgrpnmndex  17862  iccpnfcnv  23235  griedg0prc  26733  nbgrssovtx  26830  rgrusgrprc  27058  rusgrprc  27059  rgrprcx  27061  frgrwopreglem4a  27777  xrge0iifcnv  30789  0nn0m1nnn0  31961  fpprel  43397  oddinmgm  43586
  Copyright terms: Public domain W3C validator