Theorem ssd 45267

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3050  df-ss 3916

This theorem is referenced by:  iinssiin  45315  restopnssd  45338  icomnfinre  45740  fnlimfvre  45860  allbutfifvre  45861  limsupresico  45886  liminfresico  45957  limsupgtlem  45963  cnrefiisplem  46015  xlimliminflimsup  46048  rrxsnicc  46486  salrestss  46547  meaiuninclem  46666  meaiininclem  46672  borelmbl  46822  smflimlem1  46957  smflimlem2  46958  smfpimbor1lem1  46984  smfpimbor1lem2  46985  smfsuplem1  46997