|   | 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 1913 | . 2 ⊢ Ⅎ𝑥𝜑 | |
| 2 | ssd.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) | |
| 3 | 1, 2 | ssdf 45085 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 ⊆ wss 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 df-ral 3061 df-ss 3967 | 
| This theorem is referenced by: iinssiin 45139 restopnssd 45162 icomnfinre 45570 fnlimfvre 45694 allbutfifvre 45695 limsupresico 45720 liminfresico 45791 limsupgtlem 45797 cnrefiisplem 45849 xlimliminflimsup 45882 rrxsnicc 46320 salrestss 46381 meaiuninclem 46500 meaiininclem 46506 borelmbl 46656 smflimlem1 46791 smflimlem2 46792 smfpimbor1lem1 46818 smfpimbor1lem2 46819 smfsuplem1 46831 | 
| Copyright terms: Public domain | W3C validator |