Theorem pssnel 4378

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 4280	. . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
2		n0 4260	. . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
3	1, 2	sylib 221	. 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
4		eldif 3891	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
5	4	exbii 1849	. 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
6	3, 5	sylib 221	1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987   ∖ cdif 3878   ⊊ wpss 3882  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244

This theorem is referenced by:  php  8685  php3  8687  pssnn  8720  inf3lem2  9076  infpssr  9719  ssfin4  9721  genpnnp  10416  ltexprlem1  10447  reclem2pr  10459  mrieqv2d  16902  lbspss  19847  lsmcv  19906  lidlnz  19994  obslbs  20419  nmoid  23348  spansncvi  29435  fvineqsneq  34829  lsat0cv  36329  osumcllem11N  37262  pexmidlem8N  37273  isomenndlem  43169