Theorem ssd 45125

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3897

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 2180

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

This theorem is referenced by:  iinssiin  45174  restopnssd  45197  icomnfinre  45600  fnlimfvre  45720  allbutfifvre  45721  limsupresico  45746  liminfresico  45817  limsupgtlem  45823  cnrefiisplem  45875  xlimliminflimsup  45908  rrxsnicc  46346  salrestss  46407  meaiuninclem  46526  meaiininclem  46532  borelmbl  46682  smflimlem1  46817  smflimlem2  46818  smfpimbor1lem1  46844  smfpimbor1lem2  46845  smfsuplem1  46857