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

Theorem ss2rabdv 3667
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 2961 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 ss2rab 3662 . 2 ({𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒} ↔ ∀𝑥𝐴 (𝜓𝜒))
42, 3sylibr 224 1 (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  wral 2907  {crab 2911  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-in 3566  df-ss 3573
This theorem is referenced by:  sess1  5047  suppfnss  7272  suppssov1  7279  suppssfv  7283  harword  8422  mrcss  16208  ablfac1b  18401  mptscmfsupp0  18860  lspss  18916  aspss  19264  dsmmacl  20017  dsmmsubg  20019  dsmmlss  20020  scmatdmat  20253  clsss  20781  lfinpfin  21250  qustgpopn  21846  metss2lem  22239  equivcau  23021  rrxmvallem  23110  ovolsslem  23175  itg2monolem1  23440  lgamucov  24681  sqff1o  24825  musum  24834  cusgrfilem1  26255  locfinreflem  29713  omsmon  30165  orvclteinc  30342  fin2solem  33062  poimirlem26  33102  poimirlem27  33103  cnambfre  33125  pclssN  34695  2polssN  34716  dihglblem3N  36099  dochss  36169  mapdordlem2  36441  nzss  38033  rmsuppss  41465  mndpsuppss  41466  scmsuppss  41467
  Copyright terms: Public domain W3C validator