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

Theorem ss2rabdv 3832
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 3115 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 ss2rab 3827 . 2 ({𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒} ↔ ∀𝑥𝐴 (𝜓𝜒))
42, 3sylibr 224 1 (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  wral 3061  {crab 3065  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-in 3730  df-ss 3737
This theorem is referenced by:  rabssrabd  3838  sess1  5218  suppfnssOLD  7475  suppssov1  7482  suppssfv  7486  harword  8629  mrcss  16483  ablfac1b  18676  mptscmfsupp0  19137  lspss  19196  aspss  19546  dsmmacl  20301  dsmmsubg  20303  dsmmlss  20304  scmatdmat  20538  clsss  21078  lfinpfin  21547  qustgpopn  22142  metss2lem  22535  equivcau  23316  rrxmvallem  23405  ovolsslem  23471  itg2monolem1  23736  lgamucov  24984  sqff1o  25128  musum  25137  cusgrfilem1  26585  clwlknf1oclwwlknlem3  27253  locfinreflem  30246  omsmon  30699  orvclteinc  30876  fin2solem  33727  poimirlem26  33767  poimirlem27  33768  cnambfre  33789  pclssN  35702  2polssN  35723  dihglblem3N  37105  dochss  37175  mapdordlem2  37447  nzss  39042  rmsuppss  42676  mndpsuppss  42677  scmsuppss  42678
  Copyright terms: Public domain W3C validator