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

Theorem ss2rabi 3905
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 3899 . 2 ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ ∀𝑥𝐴 (𝜑𝜓))
2 ss2rabi.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprgbir 3109 1 {𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  {crab 3094  wss 3792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rab 3099  df-in 3799  df-ss 3806
This theorem is referenced by:  f1ossf1o  6660  supub  8653  suplub  8654  card2on  8748  rankval4  9027  fin1a2lem12  9568  catlid  16729  catrid  16730  gsumval2  17666  lbsextlem3  19557  psrbagsn  19891  musum  25369  ppiub  25381  umgrupgr  26451  umgrislfupgr  26471  usgruspgr  26527  usgrislfuspgr  26533  disjxwwlksn  27275  disjxwwlksnOLD  27276  clwwlknclwwlkdifnum  27360  konigsbergssiedgw  27656  omssubadd  30960  bj-unrab  33496  poimirlem26  34061  poimirlem27  34062  ssrabi  34649  lclkrs2  37694
  Copyright terms: Public domain W3C validator