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

Theorem ss2rabi 3647
 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 3641 . 2 ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ ∀𝑥𝐴 (𝜑𝜓))
2 ss2rabi.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprgbir 2911 1 {𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977  {crab 2900   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-in 3547  df-ss 3554 This theorem is referenced by:  supub  8248  suplub  8249  card2on  8342  rankval4  8613  fin1a2lem12  9116  catlid  16167  catrid  16168  gsumval2  17103  lbsextlem3  18981  psrbagsn  19316  musum  24717  ppiub  24729  umgrupgr  25769  umgrislfupgr  25789  usisuslgra  25894  disjxwwlks  26264  clwlknclwlkdifnum  26488  omssubadd  29689  bj-unrab  32114  poimirlem26  32605  poimirlem27  32606  lclkrs2  35847  usgruspgr  40408  usgrislfuspgr  40414  disjxwwlksn  41110  clwwlknclwwlkdifnum  41182  konigsbergssiedgw  41419
 Copyright terms: Public domain W3C validator