Theorem ssd 46066

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

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

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 1943  ax-6 2000  ax-7 2041  ax-12 2213

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

This theorem is used by:  iinssiin  46113  restopnssd  46136  icomnfinre  46533  fnlimfvre  46653  allbutfifvre  46654  limsupresico  46679  liminfresico  46750  limsupgtlem  46756  cnrefiisplem  46808  xlimliminflimsup  46841  fourierdlem48  47133  fourierdlem49  47134  rrxsnicc  47279  salrestss  47340  meaiuninclem  47459  meaiininclem  47465  hoicvr  47527  borelmbl  47615  smflimlem1  47750  smflimlem2  47751  smfpimbor1lem1  47777  smfpimbor1lem2  47778  smfsuplem1  47790