Theorem ssd 45528

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3054  df-ss 3900

This theorem is referenced by:  iinssiin  45576  restopnssd  45599  icomnfinre  45997  fnlimfvre  46117  allbutfifvre  46118  limsupresico  46143  liminfresico  46214  limsupgtlem  46220  cnrefiisplem  46272  xlimliminflimsup  46305  rrxsnicc  46743  salrestss  46804  meaiuninclem  46923  meaiininclem  46929  hoicvr  46991  borelmbl  47079  smflimlem1  47214  smflimlem2  47215  smfpimbor1lem1  47241  smfpimbor1lem2  47242  smfsuplem1  47254