Theorem ssd 45440

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053  df-ss 3920

This theorem is referenced by:  iinssiin  45488  restopnssd  45511  icomnfinre  45912  fnlimfvre  46032  allbutfifvre  46033  limsupresico  46058  liminfresico  46129  limsupgtlem  46135  cnrefiisplem  46187  xlimliminflimsup  46220  rrxsnicc  46658  salrestss  46719  meaiuninclem  46838  meaiininclem  46844  borelmbl  46994  smflimlem1  47129  smflimlem2  47130  smfpimbor1lem1  47156  smfpimbor1lem2  47157  smfsuplem1  47169