![]() |
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 3853 | . 2 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) |
4 | 1, 3 | mpd 15 | 1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2051 ⊆ wss 3822 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-in 3829 df-ss 3836 |
This theorem is referenced by: 0nelrel0 5458 cantnfp1lem3 8935 fpwwe2lem13 9860 pwfseqlem3 9878 hashbclem 13621 sumrblem 14926 incexclem 15049 prodrblem 15141 fprodntriv 15154 ramub1lem2 16217 mreexmrid 16784 mreexexlem2d 16786 acsfiindd 17657 lbspss 19588 lbsextlem4 19667 lindfrn 20682 fclscmpi 22356 lhop2 24330 lhop 24331 dvcnvrelem1 24332 axlowdimlem17 26462 cyc3co2 30491 erdszelem8 32067 bj-fununsn1 34041 bj-fvsnun2 34044 osumcllem10N 36583 pexmidlem7N 36594 mapdindp2 38339 mapdindp3 38340 hdmapval3lemN 38455 hdmap11lem1 38459 fourierdlem80 41936 |
Copyright terms: Public domain | W3C validator |