Theorem nss 3956

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

Step	Hyp	Ref	Expression
1		exanali 1844	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		dfss2 3883	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 336	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ¬ 𝐴 ⊆ 𝐵)
4	3	bicomi 225	1 ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1523  ∃wex 1765   ∈ wcel 2083   ⊆ wss 3865

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-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880

This theorem is referenced by:  grur1  10095  psslinpr  10306  reclem2pr  10323  mreexexlem2d  16749  prmcyg  18739  filconn  22179  alexsubALTlem4  22346  wilthlem2  25332  shne0i  28912  erdszelem10  32057  fundmpss  32619  ntrneineine1lem  39940  nssrex  40911  nssd  40932  nsssmfmbf  42619