Theorem pssnel 4401

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 4297	. . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
2		n0 4277	. . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
3	1, 2	sylib 217	. 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴))
4		eldif 3893	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
5	4	exbii 1851	. 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))
6	3, 5	sylib 217	1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942   ∖ cdif 3880   ⊊ wpss 3884  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254

This theorem is referenced by:  php  8897  php3  8899  pssnn  8913  pssnnOLD  8969  inf3lem2  9317  infpssr  9995  ssfin4  9997  genpnnp  10692  ltexprlem1  10723  reclem2pr  10735  mrieqv2d  17265  lbspss  20259  lsmcv  20318  lidlnz  20412  obslbs  20847  nmoid  23812  spansncvi  29915  fvineqsneq  35510  lsat0cv  36974  osumcllem11N  37907  pexmidlem8N  37918  isomenndlem  43958