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 41499
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 1915 . 2 𝑥𝜑
2 ssd.1 . 2 ((𝜑𝑥𝐴) → 𝑥𝐵)
31, 2ssdf 41494 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2114  wss 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-ral 3130  df-v 3475  df-in 3920  df-ss 3930
This theorem is referenced by:  iinssiin  41549  funimassd  41651  icomnfinre  41980  fnlimfvre  42107  allbutfifvre  42108  limsupresico  42133  liminfresico  42204  limsupgtlem  42210  cnrefiisplem  42262  xlimliminflimsup  42295  rrxsnicc  42733  meaiuninclem  42910  meaiininclem  42916  borelmbl  43066  smflimlem1  43195  smflimlem2  43196  smfpimbor1lem1  43221  smfpimbor1lem2  43222  smfsuplem1  43233
  Copyright terms: Public domain W3C validator