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

Theorem ss2rabdv 4034
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 3140 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 ss2rab 4029 . 2 ({𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒} ↔ ∀𝑥𝐴 (𝜓𝜒))
42, 3sylibr 233 1 (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3061  {crab 3406  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rab 3407  df-v 3446  df-in 3918  df-ss 3928
This theorem is referenced by:  rabssrabd  4042  sess1  5602  suppssov1  8130  suppssfv  8134  cofon1  8619  naddssim  8632  harword  9504  scottex  9826  mrcss  17501  ablfac1b  19854  mptscmfsupp0  20402  lspss  20460  dsmmacl  21163  dsmmsubg  21165  dsmmlss  21166  aspss  21296  scmatdmat  21880  clsss  22421  lfinpfin  22891  qustgpopn  23487  metss2lem  23883  equivcau  24680  rrxmvallem  24784  ovolsslem  24864  itg2monolem1  25131  lgamucov  26403  sqff1o  26547  musum  26556  madess  27228  cofcut1  27261  cusgrfilem1  28445  clwlknf1oclwwlknlem3  29069  occon  30271  spanss  30332  rmfsupp2  32122  fldgenss  32131  locfinreflem  32478  omsmon  32955  orvclteinc  33132  fin2solem  36110  poimirlem26  36150  poimirlem27  36151  cnambfre  36172  pclssN  38403  2polssN  38424  dihglblem3N  39804  dochss  39874  mapdordlem2  40146  nna4b4nsq  41041  itgoss  41533  nzss  42685  ovnsslelem  44887  rmsuppss  46532  mndpsuppss  46533  scmsuppss  46534
  Copyright terms: Public domain W3C validator