Theorem ssd 45691

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-ral 3086  df-ss 3930

This theorem is referenced by:  iinssiin  45738  restopnssd  45761  icomnfinre  46159  fnlimfvre  46279  allbutfifvre  46280  limsupresico  46305  liminfresico  46376  limsupgtlem  46382  cnrefiisplem  46434  xlimliminflimsup  46467  fourierdlem48  46759  fourierdlem49  46760  rrxsnicc  46905  salrestss  46966  meaiuninclem  47085  meaiininclem  47091  hoicvr  47153  borelmbl  47241  smflimlem1  47376  smflimlem2  47377  smfpimbor1lem1  47403  smfpimbor1lem2  47404  smfsuplem1  47416