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

Theorem nss 4042
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 1855 . . 3 (∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) ↔ ¬ ∀𝑥(𝑥𝐴𝑥𝐵))
2 dfss2 3964 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2xchbinxr 335 . 2 (∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) ↔ ¬ 𝐴𝐵)
43bicomi 223 1 𝐴𝐵 ↔ ∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wal 1532  wex 1774  wcel 2099  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961
This theorem is referenced by:  grur1  10835  psslinpr  11046  reclem2pr  11063  mreexexlem2d  17616  prmcyg  19840  filconn  23774  alexsubALTlem4  23941  wilthlem2  26988  shne0i  31245  erdszelem10  34746  fundmpss  35298  ntrneineine1lem  43437  nssrex  44375  nssd  44394  nsssmfmbf  46090
  Copyright terms: Public domain W3C validator