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 3965 | . 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)) |
3 | 2 | con3d 155 | 1 ⊢ (𝜑 → (¬ 𝐶 ∈ 𝐵 → ¬ 𝐶 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2110 ⊆ wss 3935 |
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 2157 ax-12 2173 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-in 3942 df-ss 3951 |
This theorem is referenced by: ssneldd 3969 kmlem2 9571 hashbclem 13804 prodss 15295 coprmproddvdslem 16000 mrissmrid 16906 mpfrcl 20292 onsuct0 33784 ftc1anc 34969 dvhdimlem 38574 dvh3dim2 38578 dvh3dim3N 38579 mapdh9a 38919 hdmapval0 38963 hdmap11lem2 38972 iundjiunlem 42735 elbigolo1 44611 |
Copyright terms: Public domain | W3C validator |