![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssneldd | Structured version Visualization version GIF version |
Description: If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ssneld.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
ssneldd.2 | ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) |
Ref | Expression |
---|---|
ssneldd | ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssneldd.2 | . 2 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) | |
2 | ssneld.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
3 | 2 | ssneld 3976 | . 2 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) |
4 | 1, 3 | mpd 15 | 1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2098 ⊆ wss 3940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-v 3468 df-in 3947 df-ss 3957 |
This theorem is referenced by: 0nelrel0 5726 cantnfp1lem3 9670 fpwwe2lem12 10632 pwfseqlem3 10650 hashbclem 14407 sumrblem 15653 incexclem 15778 prodrblem 15869 fprodntriv 15882 ramub1lem2 16956 mreexmrid 17583 mreexexlem2d 17585 acsfiindd 18505 lbspss 20915 lbsextlem4 20997 lindfrn 21676 fclscmpi 23843 lhop2 25858 lhop 25859 dvcnvrelem1 25860 axlowdimlem17 28640 cyc3co2 32726 erdszelem8 34644 bj-fununsn1 36590 bj-fvsnun2 36593 poimirlem16 36960 osumcllem10N 39292 pexmidlem7N 39303 mapdindp2 41048 mapdindp3 41049 hdmapval3lemN 41164 hdmap11lem1 41168 fourierdlem80 45353 |
Copyright terms: Public domain | W3C validator |