Theorem ssd 45532

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

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

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 3053  df-ss 3907

This theorem is referenced by:  iinssiin  45580  restopnssd  45603  icomnfinre  46003  fnlimfvre  46123  allbutfifvre  46124  limsupresico  46149  liminfresico  46220  limsupgtlem  46226  cnrefiisplem  46278  xlimliminflimsup  46311  rrxsnicc  46749  salrestss  46810  meaiuninclem  46929  meaiininclem  46935  hoicvr  46997  borelmbl  47085  smflimlem1  47220  smflimlem2  47221  smfpimbor1lem1  47247  smfpimbor1lem2  47248  smfsuplem1  47260