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 2737 . 2 (𝐴 = 𝐵𝐶 = 𝐶)
31, 2neleq12d 3041 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1541  wnel 3036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-nel 3037
This theorem is referenced by:  ruALT  9511  ssnn0fi  13908  cnpart  15163  sqrmo  15174  resqrtcl  15176  resqrtthlem  15177  sqrtneg  15190  sqreu  15284  sqrtthlem  15286  eqsqrtd  15291  ge2nprmge4  16628  prmgaplem7  16985  mgmnsgrpex  18856  sgrpnmndex  18857  iccpnfcnv  24898  griedg0prc  29337  nbgrssovtx  29434  rgrusgrprc  29663  rusgrprc  29664  rgrprcx  29666  frgrwopreglem4a  30385  xrge0iifcnv  34090  0nn0m1nnn0  35307  fpprel  47970  gpg5nbgrvtx03star  48322  gpg5nbgr3star  48323  grlimedgnedg  48373  oddinmgm  48417
  Copyright terms: Public domain W3C validator