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

Theorem ss2rabdv 4003
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 3106 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 ss2rab 3998 . 2 ({𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒} ↔ ∀𝑥𝐴 (𝜓𝜒))
42, 3sylibr 237 1 (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2111  wral 3062  {crab 3066  wss 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ral 3067  df-rab 3071  df-v 3422  df-in 3887  df-ss 3897
This theorem is referenced by:  rabssrabd  4010  sess1  5533  suppssov1  7960  suppssfv  7964  harword  9203  mrcss  17143  ablfac1b  19481  mptscmfsupp0  19988  lspss  20045  dsmmacl  20727  dsmmsubg  20729  dsmmlss  20730  aspss  20860  scmatdmat  21436  clsss  21975  lfinpfin  22445  qustgpopn  23041  metss2lem  23433  equivcau  24221  rrxmvallem  24325  ovolsslem  24405  itg2monolem1  24672  lgamucov  25944  sqff1o  26088  musum  26097  cusgrfilem1  27567  clwlknf1oclwwlknlem3  28190  rmfsupp2  31235  locfinreflem  31528  omsmon  32001  orvclteinc  32178  naddssim  33600  madess  33822  cofcut1  33853  fin2solem  35526  poimirlem26  35566  poimirlem27  35567  cnambfre  35588  pclssN  37671  2polssN  37692  dihglblem3N  39072  dochss  39142  mapdordlem2  39414  nna4b4nsq  40228  nzss  41636  rmsuppss  45407  mndpsuppss  45408  scmsuppss  45409
  Copyright terms: Public domain W3C validator