Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssd Structured version   Visualization version   GIF version

Theorem ssd 45090
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
StepHypRef Expression
1 nfv 1913 . 2 𝑥𝜑
2 ssd.1 . 2 ((𝜑𝑥𝐴) → 𝑥𝐵)
31, 2ssdf 45085 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2107  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-ral 3061  df-ss 3967
This theorem is referenced by:  iinssiin  45139  restopnssd  45162  icomnfinre  45570  fnlimfvre  45694  allbutfifvre  45695  limsupresico  45720  liminfresico  45791  limsupgtlem  45797  cnrefiisplem  45849  xlimliminflimsup  45882  rrxsnicc  46320  salrestss  46381  meaiuninclem  46500  meaiininclem  46506  borelmbl  46656  smflimlem1  46791  smflimlem2  46792  smfpimbor1lem1  46818  smfpimbor1lem2  46819  smfsuplem1  46831
  Copyright terms: Public domain W3C validator