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

Theorem nss 4059
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 1856 . . 3 (∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) ↔ ¬ ∀𝑥(𝑥𝐴𝑥𝐵))
2 df-ss 3979 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2xchbinxr 335 . 2 (∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵) ↔ ¬ 𝐴𝐵)
43bicomi 224 1 𝐴𝐵 ↔ ∃𝑥(𝑥𝐴 ∧ ¬ 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1534  wex 1775  wcel 2105  wss 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-ss 3979
This theorem is referenced by:  grur1  10857  psslinpr  11068  reclem2pr  11085  mreexexlem2d  17689  prmcyg  19926  filconn  23906  alexsubALTlem4  24073  wilthlem2  27126  shne0i  31476  erdszelem10  35184  fundmpss  35747  ntrneineine1lem  44073  nssrex  45025  nssd  45044  nsssmfmbf  46734
  Copyright terms: Public domain W3C validator