| 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 4369 | . . 3 ⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | |
| 2 | n0 4353 | . . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) | |
| 3 | 1, 2 | sylib 218 | . 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) |
| 4 | eldif 3961 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
| 5 | 4 | exbii 1848 | . 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
| 6 | 3, 5 | sylib 218 | 1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ≠ wne 2940 ∖ cdif 3948 ⊊ wpss 3952 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-v 3482 df-dif 3954 df-ss 3968 df-pss 3971 df-nul 4334 |
| This theorem is referenced by: pssnn 9208 php 9247 php3 9249 phpOLD 9259 php3OLD 9261 inf3lem2 9669 infpssr 10348 ssfin4 10350 genpnnp 11045 ltexprlem1 11076 reclem2pr 11088 mrieqv2d 17682 lbspss 21081 lsmcv 21143 lidlnz 21252 obslbs 21750 nmoid 24763 spansncvi 31671 fvineqsneq 37413 lsat0cv 39034 osumcllem11N 39968 pexmidlem8N 39979 isomenndlem 46545 |
| Copyright terms: Public domain | W3C validator |