Theorem ssd 46233

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077  df-ss 3897

This theorem is used by:  iinssiin  46280  restopnssd  46303  icomnfinre  46700  fnlimfvre  46820  allbutfifvre  46821  limsupresico  46846  liminfresico  46917  limsupgtlem  46923  cnrefiisplem  46975  xlimliminflimsup  47008  fourierdlem48  47300  fourierdlem49  47301  rrxsnicc  47446  salrestss  47507  meaiuninclem  47626  meaiininclem  47632  hoicvr  47694  borelmbl  47782  smflimlem1  47917  smflimlem2  47918  smfpimbor1lem1  47944  smfpimbor1lem2  47945  smfsuplem1  47957