Theorem ssd 46370

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081  df-ss 3901

This theorem is used by:  iinssiin  46417  restopnssd  46440  icomnfinre  46837  fnlimfvre  46957  allbutfifvre  46958  limsupresico  46983  liminfresico  47054  limsupgtlem  47060  cnrefiisplem  47112  xlimliminflimsup  47145  fourierdlem48  47437  fourierdlem49  47438  rrxsnicc  47583  salrestss  47644  meaiuninclem  47763  meaiininclem  47769  hoicvr  47831  borelmbl  47919  smflimlem1  48054  smflimlem2  48055  smfpimbor1lem1  48081  smfpimbor1lem2  48082  smfsuplem1  48094