Theorem ssd 45858

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

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

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 2216

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

This theorem is used by:  iinssiin  45905  restopnssd  45928  icomnfinre  46326  fnlimfvre  46446  allbutfifvre  46447  limsupresico  46472  liminfresico  46543  limsupgtlem  46549  cnrefiisplem  46601  xlimliminflimsup  46634  fourierdlem48  46926  fourierdlem49  46927  rrxsnicc  47072  salrestss  47133  meaiuninclem  47252  meaiininclem  47258  hoicvr  47320  borelmbl  47408  smflimlem1  47543  smflimlem2  47544  smfpimbor1lem1  47570  smfpimbor1lem2  47571  smfsuplem1  47583