Theorem ssd 45800

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-ral 3080  df-ss 3922

This theorem is referenced by:  iinssiin  45847  restopnssd  45870  icomnfinre  46268  fnlimfvre  46388  allbutfifvre  46389  limsupresico  46414  liminfresico  46485  limsupgtlem  46491  cnrefiisplem  46543  xlimliminflimsup  46576  fourierdlem48  46868  fourierdlem49  46869  rrxsnicc  47014  salrestss  47075  meaiuninclem  47194  meaiininclem  47200  hoicvr  47262  borelmbl  47350  smflimlem1  47485  smflimlem2  47486  smfpimbor1lem1  47512  smfpimbor1lem2  47513  smfsuplem1  47525