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 4310 | . . 3 ⊢ ((𝐵 ∖ 𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) | |
3 | 1, 2 | sylib 220 | . 2 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴)) |
4 | eldif 3946 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
5 | 4 | exbii 1844 | . 2 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
6 | 3, 5 | sylib 220 | 1 ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∃wex 1776 ∈ wcel 2110 ≠ wne 3016 ∖ cdif 3933 ⊊ wpss 3937 ∅c0 4291 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-v 3497 df-dif 3939 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 |
This theorem is referenced by: php 8695 php3 8697 pssnn 8730 inf3lem2 9086 infpssr 9724 ssfin4 9726 genpnnp 10421 ltexprlem1 10452 reclem2pr 10464 mrieqv2d 16904 lbspss 19848 lsmcv 19907 lidlnz 19995 obslbs 20868 nmoid 23345 spansncvi 29423 fvineqsneq 34687 lsat0cv 36163 osumcllem11N 37096 pexmidlem8N 37107 isomenndlem 42805 |
Copyright terms: Public domain | W3C validator |