![]() |
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 4367 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | |
2 | n0 4347 | . . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) | |
3 | 1, 2 | sylib 217 | . 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) |
4 | eldif 3959 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
5 | 4 | exbii 1851 | . 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
6 | 3, 5 | sylib 217 | 1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ≠ wne 2941 ∖ cdif 3946 ⊊ wpss 3950 ∅c0 4323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-v 3477 df-dif 3952 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 |
This theorem is referenced by: pssnn 9168 php 9210 php3 9212 phpOLD 9222 php3OLD 9224 pssnnOLD 9265 inf3lem2 9624 infpssr 10303 ssfin4 10305 genpnnp 11000 ltexprlem1 11031 reclem2pr 11043 mrieqv2d 17583 lbspss 20693 lsmcv 20754 lidlnz 20853 obslbs 21285 nmoid 24259 spansncvi 30905 fvineqsneq 36293 lsat0cv 37903 osumcllem11N 38837 pexmidlem8N 38848 isomenndlem 45246 |
Copyright terms: Public domain | W3C validator |