![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pssnel | Structured version Visualization version GIF version |
Description: A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.) |
Ref | Expression |
---|---|
pssnel | ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pssdif 4326 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | |
2 | n0 4306 | . . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) | |
3 | 1, 2 | sylib 217 | . 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) |
4 | eldif 3920 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
5 | 4 | exbii 1850 | . 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
6 | 3, 5 | sylib 217 | 1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∃wex 1781 ∈ wcel 2106 ≠ wne 2943 ∖ cdif 3907 ⊊ wpss 3911 ∅c0 4282 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2944 df-v 3447 df-dif 3913 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 |
This theorem is referenced by: pssnn 9112 php 9154 php3 9156 phpOLD 9166 php3OLD 9168 pssnnOLD 9209 inf3lem2 9565 infpssr 10244 ssfin4 10246 genpnnp 10941 ltexprlem1 10972 reclem2pr 10984 mrieqv2d 17519 lbspss 20543 lsmcv 20602 lidlnz 20698 obslbs 21136 nmoid 24106 spansncvi 30594 fvineqsneq 35883 lsat0cv 37495 osumcllem11N 38429 pexmidlem8N 38440 isomenndlem 44761 |
Copyright terms: Public domain | W3C validator |