Theorem ssd 45074

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045  df-ss 3931

This theorem is referenced by:  iinssiin  45123  restopnssd  45146  icomnfinre  45550  fnlimfvre  45672  allbutfifvre  45673  limsupresico  45698  liminfresico  45769  limsupgtlem  45775  cnrefiisplem  45827  xlimliminflimsup  45860  rrxsnicc  46298  salrestss  46359  meaiuninclem  46478  meaiininclem  46484  borelmbl  46634  smflimlem1  46769  smflimlem2  46770  smfpimbor1lem1  46796  smfpimbor1lem2  46797  smfsuplem1  46809