![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ssd | Structured version Visualization version GIF version |
Description: A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
Ref | Expression |
---|---|
ssd.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
Ref | Expression |
---|---|
ssd | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1909 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ssd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) | |
3 | 1, 2 | ssdf 44578 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 ⊆ wss 3944 |
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-12 2166 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-nf 1778 df-ral 3051 df-ss 3961 |
This theorem is referenced by: iinssiin 44632 restopnssd 44659 icomnfinre 45072 fnlimfvre 45197 allbutfifvre 45198 limsupresico 45223 liminfresico 45294 limsupgtlem 45300 cnrefiisplem 45352 xlimliminflimsup 45385 rrxsnicc 45823 salrestss 45884 meaiuninclem 46003 meaiininclem 46009 borelmbl 46159 smflimlem1 46294 smflimlem2 46295 smfpimbor1lem1 46321 smfpimbor1lem2 46322 smfsuplem1 46334 |
Copyright terms: Public domain | W3C validator |