Theorem ssd 45071

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 45066	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

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

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 3053  df-ss 3948

This theorem is referenced by:  iinssiin  45120  restopnssd  45143  icomnfinre  45548  fnlimfvre  45670  allbutfifvre  45671  limsupresico  45696  liminfresico  45767  limsupgtlem  45773  cnrefiisplem  45825  xlimliminflimsup  45858  rrxsnicc  46296  salrestss  46357  meaiuninclem  46476  meaiininclem  46482  borelmbl  46632  smflimlem1  46767  smflimlem2  46768  smfpimbor1lem1  46794  smfpimbor1lem2  46795  smfsuplem1  46807