Theorem ssd 45090

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-ral 3061  df-ss 3967

This theorem is referenced by:  iinssiin  45139  restopnssd  45162  icomnfinre  45570  fnlimfvre  45694  allbutfifvre  45695  limsupresico  45720  liminfresico  45791  limsupgtlem  45797  cnrefiisplem  45849  xlimliminflimsup  45882  rrxsnicc  46320  salrestss  46381  meaiuninclem  46500  meaiininclem  46506  borelmbl  46656  smflimlem1  46791  smflimlem2  46792  smfpimbor1lem1  46818  smfpimbor1lem2  46819  smfsuplem1  46831