Theorem pssnel 4423

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932   ∖ cdif 3898   ⊊ wpss 3902  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-ss 3918  df-pss 3921  df-nul 4286

This theorem is referenced by:  pssnn  9093  php  9131  php3  9133  inf3lem2  9538  infpssr  10218  ssfin4  10220  genpnnp  10916  ltexprlem1  10947  reclem2pr  10959  mrieqv2d  17562  lbspss  21034  lsmcv  21096  lidlnz  21197  obslbs  21685  nmoid  24686  spansncvi  31727  fvineqsneq  37617  lsat0cv  39303  osumcllem11N  40236  pexmidlem8N  40247  isomenndlem  46784