Theorem pssnel 4446

Description: A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)

Assertion

Ref	Expression
pssnel	⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem pssnel

Step	Hyp	Ref	Expression
1		pssdif 4344	. . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
2		n0 4328	. . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
3	1, 2	sylib 218	. 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
4		eldif 3936	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
5	4	exbii 1848	. 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
6	3, 5	sylib 218	1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108   ≠ wne 2932   ∖ cdif 3923   ⊊ wpss 3927  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-ss 3943  df-pss 3946  df-nul 4309

This theorem is referenced by:  pssnn  9182  php  9221  php3  9223  phpOLD  9231  php3OLD  9233  inf3lem2  9643  infpssr  10322  ssfin4  10324  genpnnp  11019  ltexprlem1  11050  reclem2pr  11062  mrieqv2d  17651  lbspss  21040  lsmcv  21102  lidlnz  21203  obslbs  21690  nmoid  24681  spansncvi  31633  fvineqsneq  37430  lsat0cv  39051  osumcllem11N  39985  pexmidlem8N  39996  isomenndlem  46559