Theorem ssd 44583

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 1909	. 2 ⊢ Ⅎ𝑥𝜑
2		ssd.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
3	1, 2	ssdf 44578	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

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