Theorem pssnel 4367

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 4265	. . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
2		n0 4245	. . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
3	1, 2	sylib 221	. 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
4		eldif 3868	. . 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 2951   ∖ cdif 3855   ⊊ wpss 3859  ∅c0 4225

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 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-v 3411  df-dif 3861  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226

This theorem is referenced by:  php  8723  php3  8725  pssnn  8738  pssnnOLD  8774  inf3lem2  9125  infpssr  9768  ssfin4  9770  genpnnp  10465  ltexprlem1  10496  reclem2pr  10508  mrieqv2d  16968  lbspss  19922  lsmcv  19981  lidlnz  20069  obslbs  20495  nmoid  23444  spansncvi  29534  fvineqsneq  35109  lsat0cv  36609  osumcllem11N  37542  pexmidlem8N  37553  isomenndlem  43535