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

Theorem nss 4026
Description: Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18. (Contributed by NM, 25-Feb-1996.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
nss 𝐴𝐵 ↔ ∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem nss
StepHypRef Expression
1 exanali 1850 . . 3 (∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) ↔ ¬ ∀𝑥(𝑥𝐴𝑥𝐵))
2 dfss2 3952 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2xchbinxr 336 . 2 (∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) ↔ ¬ 𝐴𝐵)
43bicomi 225 1 𝐴𝐵 ↔ ∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526  wex 1771  wcel 2105  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  grur1  10230  psslinpr  10441  reclem2pr  10458  mreexexlem2d  16904  prmcyg  18943  filconn  22419  alexsubALTlem4  22586  wilthlem2  25573  shne0i  29152  erdszelem10  32344  fundmpss  32906  ntrneineine1lem  40312  nssrex  41228  nssd  41248  nsssmfmbf  42932
  Copyright terms: Public domain W3C validator