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 39566
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 1883 . 2 𝑥𝜑
2 ssd.1 . 2 ((𝜑𝑥𝐴) → 𝑥𝐵)
31, 2ssdf 39561 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-in 3614  df-ss 3621
This theorem is referenced by:  funimassd  39745  icomnfinre  40097  fnlimfvre  40224  allbutfifvre  40225  limsupresico  40250  liminfresico  40321  limsupgtlem  40327  cnrefiisplem  40373  rrxsnicc  40838  meaiuninclem  41015  meaiininclem  41021  borelmbl  41171  smflimlem1  41300  smflimlem2  41301  smfpimbor1lem1  41326  smfpimbor1lem2  41327  smfsuplem1  41338
  Copyright terms: Public domain W3C validator