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

Theorem ss2rabdv 3824
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 3104 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 ss2rab 3819 . 2 ({𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒} ↔ ∀𝑥𝐴 (𝜓𝜒))
42, 3sylibr 224 1 (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139  wral 3050  {crab 3054  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-in 3722  df-ss 3729
This theorem is referenced by:  rabssrabd  3830  sess1  5234  suppfnssOLD  7489  suppssov1  7496  suppssfv  7500  harword  8635  mrcss  16478  ablfac1b  18669  mptscmfsupp0  19130  lspss  19186  aspss  19534  dsmmacl  20287  dsmmsubg  20289  dsmmlss  20290  scmatdmat  20523  clsss  21060  lfinpfin  21529  qustgpopn  22124  metss2lem  22517  equivcau  23298  rrxmvallem  23387  ovolsslem  23452  itg2monolem1  23716  lgamucov  24963  sqff1o  25107  musum  25116  cusgrfilem1  26561  clwlknf1oclwwlknlem3  27227  clwwlknonclwlknonf1olem  27521  locfinreflem  30216  omsmon  30669  orvclteinc  30846  fin2solem  33708  poimirlem26  33748  poimirlem27  33749  cnambfre  33771  pclssN  35683  2polssN  35704  dihglblem3N  37086  dochss  37156  mapdordlem2  37428  nzss  39018  rmsuppss  42661  mndpsuppss  42662  scmsuppss  42663
  Copyright terms: Public domain W3C validator