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 3903 | . 2 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) |
4 | 1, 3 | mpd 15 | 1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2110 ⊆ wss 3866 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 |
This theorem is referenced by: 0nelrel0 5609 cantnfp1lem3 9295 fpwwe2lem12 10256 pwfseqlem3 10274 hashbclem 14016 sumrblem 15275 incexclem 15400 prodrblem 15491 fprodntriv 15504 ramub1lem2 16580 mreexmrid 17146 mreexexlem2d 17148 acsfiindd 18059 lbspss 20119 lbsextlem4 20198 lindfrn 20783 fclscmpi 22926 lhop2 24912 lhop 24913 dvcnvrelem1 24914 axlowdimlem17 27049 cyc3co2 31126 erdszelem8 32873 bj-fununsn1 35159 bj-fvsnun2 35162 poimirlem16 35530 osumcllem10N 37716 pexmidlem7N 37727 mapdindp2 39472 mapdindp3 39473 hdmapval3lemN 39588 hdmap11lem1 39592 fourierdlem80 43402 |
Copyright terms: Public domain | W3C validator |