Theorem ssd 45914

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 45909	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 3077  df-ss 3916

This theorem is used by:  iinssiin  45961  restopnssd  45984  icomnfinre  46382  fnlimfvre  46502  allbutfifvre  46503  limsupresico  46528  liminfresico  46599  limsupgtlem  46605  cnrefiisplem  46657  xlimliminflimsup  46690  fourierdlem48  46982  fourierdlem49  46983  rrxsnicc  47128  salrestss  47189  meaiuninclem  47308  meaiininclem  47314  hoicvr  47376  borelmbl  47464  smflimlem1  47599  smflimlem2  47600  smfpimbor1lem1  47626  smfpimbor1lem2  47627  smfsuplem1  47639