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  6662  supub  8655  suplub  8656  card2on  8750  rankval4  9029  fin1a2lem12  9570  catlid  16733  catrid  16734  gsumval2  17670  lbsextlem3  19561  psrbagsn  19895  musum  25373  ppiub  25385  umgrupgr  26455  umgrislfupgr  26475  usgruspgr  26531  usgrislfuspgr  26537  disjxwwlksn  27279  disjxwwlksnOLD  27280  clwwlknclwwlkdifnum  27364  konigsbergssiedgw  27660  omssubadd  30964  bj-unrab  33500  poimirlem26  34066  poimirlem27  34067  ssrabi  34654  lclkrs2  37699
 Copyright terms: Public domain W3C validator