Theorem ssd 45325

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3052  df-ss 3918

This theorem is referenced by:  iinssiin  45373  restopnssd  45396  icomnfinre  45798  fnlimfvre  45918  allbutfifvre  45919  limsupresico  45944  liminfresico  46015  limsupgtlem  46021  cnrefiisplem  46073  xlimliminflimsup  46106  rrxsnicc  46544  salrestss  46605  meaiuninclem  46724  meaiininclem  46730  borelmbl  46880  smflimlem1  47015  smflimlem2  47016  smfpimbor1lem1  47042  smfpimbor1lem2  47043  smfsuplem1  47055