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 44583
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 1909 . 2 𝑥𝜑
2 ssd.1 . 2 ((𝜑𝑥𝐴) → 𝑥𝐵)
31, 2ssdf 44578 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2098  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-nf 1778  df-ral 3051  df-ss 3961
This theorem is referenced by:  iinssiin  44632  restopnssd  44659  icomnfinre  45072  fnlimfvre  45197  allbutfifvre  45198  limsupresico  45223  liminfresico  45294  limsupgtlem  45300  cnrefiisplem  45352  xlimliminflimsup  45385  rrxsnicc  45823  salrestss  45884  meaiuninclem  46003  meaiininclem  46009  borelmbl  46159  smflimlem1  46294  smflimlem2  46295  smfpimbor1lem1  46321  smfpimbor1lem2  46322  smfsuplem1  46334
  Copyright terms: Public domain W3C validator