Theorem nss 4000

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 1878	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		df-ss 3921	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 337	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ¬ 𝐴 ⊆ 𝐵)
4	3	bicomi 226	1 ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557  ∃wex 1798   ∈ wcel 2141   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ss 3921

This theorem is referenced by:  nssrex  4001  grur1  10775  psslinpr  10986  reclem2pr  11003  mreexexlem2d  17660  prmcyg  19917  filconn  23923  alexsubALTlem4  24090  wilthlem2  27110  shne0i  31597  onvf1odlem2  35411  erdszelem10  35514  fundmpss  36081  ntrneineine1lem  44624  nssd  45647  nsssmfmbf  47317