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

Theorem ss2rabi 4028
Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)
Hypothesis
Ref Expression
ss2rabi.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ss2rabi {𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓}

Proof of Theorem ss2rabi
StepHypRef Expression
1 ss2rab 4022 . 2 ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ ∀𝑥𝐴 (𝜑𝜓))
2 ss2rabi.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprgbir 3145 1 {𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  {crab 3134  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rab 3139  df-v 3471  df-in 3915  df-ss 3925
This theorem is referenced by:  f1ossf1o  6872  supub  8911  suplub  8912  card2on  9006  rankval4  9284  fin1a2lem12  9822  catlid  16945  catrid  16946  gsumval2  17887  lbsextlem3  19923  psrbagsn  20732  musum  25774  ppiub  25786  umgrupgr  26894  umgrislfupgr  26914  usgruspgr  26969  usgrislfuspgr  26975  disjxwwlksn  27688  clwwlknclwwlkdifnum  27763  konigsbergssiedgw  28033  omssubadd  31632  bj-unrab  34329  poimirlem26  35041  poimirlem27  35042  ssrabi  35629  lclkrs2  38794
  Copyright terms: Public domain W3C validator