![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssneld | Structured version Visualization version GIF version |
Description: If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ssneld.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
ssneld | ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssneld.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | 1 | sseld 3994 | . 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
3 | 2 | con3d 152 | 1 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2106 ⊆ wss 3963 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-clel 2814 df-ss 3980 |
This theorem is referenced by: ssneldd 3998 kmlem2 10190 hashbclem 14488 prodss 15980 coprmproddvdslem 16696 mrissmrid 17686 mpfrcl 22127 onsuct0 36424 ftc1anc 37688 dvhdimlem 41427 dvh3dim2 41431 dvh3dim3N 41432 mapdh9a 41772 hdmapval0 41816 hdmap11lem2 41825 iundjiunlem 46415 elbigolo1 48407 |
Copyright terms: Public domain | W3C validator |