Theorem ssd 45613

Description: A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)

Hypothesis

Ref	Expression
ssd.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
ssd	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem ssd

Step	Hyp	Ref	Expression
1		nfv 1933	. 2 ⊢ Ⅎ𝑥𝜑
2		ssd.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
3	1, 2	ssdf 45608	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-ral 3076  df-ss 3921

This theorem is referenced by:  iinssiin  45660  restopnssd  45683  icomnfinre  46081  fnlimfvre  46201  allbutfifvre  46202  limsupresico  46227  liminfresico  46298  limsupgtlem  46304  cnrefiisplem  46356  xlimliminflimsup  46389  rrxsnicc  46827  salrestss  46888  meaiuninclem  47007  meaiininclem  47013  hoicvr  47075  borelmbl  47163  smflimlem1  47298  smflimlem2  47299  smfpimbor1lem1  47325  smfpimbor1lem2  47326  smfsuplem1  47338