MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2rabdv Structured version   Visualization version   GIF version

Theorem ss2rabdv 4028
Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)
Hypothesis
Ref Expression
ss2rabdv.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ss2rabdv (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ss2rabdv
StepHypRef Expression
1 ss2rabdv.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ralrimiva 3170 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 ss2rab 4023 . 2 ({𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒} ↔ ∀𝑥𝐴 (𝜓𝜒))
42, 3sylibr 237 1 (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  wral 3126  {crab 3130  wss 3910
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rab 3135  df-v 3473  df-in 3917  df-ss 3927
This theorem is referenced by:  rabssrabd  4034  sess1  5496  suppssov1  7837  suppssfv  7841  harword  9003  mrcss  16866  ablfac1b  19171  mptscmfsupp0  19675  lspss  19732  aspss  20082  dsmmacl  20861  dsmmsubg  20863  dsmmlss  20864  scmatdmat  21100  clsss  21638  lfinpfin  22108  qustgpopn  22704  metss2lem  23097  equivcau  23883  rrxmvallem  23987  ovolsslem  24067  itg2monolem1  24333  lgamucov  25602  sqff1o  25746  musum  25755  cusgrfilem1  27224  clwlknf1oclwwlknlem3  27847  rmfsupp2  30874  locfinreflem  31115  omsmon  31564  orvclteinc  31741  fin2solem  34925  poimirlem26  34965  poimirlem27  34966  cnambfre  34987  pclssN  37072  2polssN  37093  dihglblem3N  38473  dochss  38543  mapdordlem2  38815  nzss  40832  rmsuppss  44590  mndpsuppss  44591  scmsuppss  44592
  Copyright terms: Public domain W3C validator