Theorem ssd 45511

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3052  df-ss 3906

This theorem is referenced by:  iinssiin  45559  restopnssd  45582  icomnfinre  45982  fnlimfvre  46102  allbutfifvre  46103  limsupresico  46128  liminfresico  46199  limsupgtlem  46205  cnrefiisplem  46257  xlimliminflimsup  46290  rrxsnicc  46728  salrestss  46789  meaiuninclem  46908  meaiininclem  46914  hoicvr  46976  borelmbl  47064  smflimlem1  47199  smflimlem2  47200  smfpimbor1lem1  47226  smfpimbor1lem2  47227  smfsuplem1  47239