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

Theorem ss2rabi 3817
 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 3811 . 2 ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ ∀𝑥𝐴 (𝜑𝜓))
2 ss2rabi.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2mprgbir 3057 1 {𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2131  {crab 3046   ⊆ wss 3707 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rab 3051  df-in 3714  df-ss 3721 This theorem is referenced by:  supub  8522  suplub  8523  card2on  8616  rankval4  8895  fin1a2lem12  9417  catlid  16537  catrid  16538  gsumval2  17473  lbsextlem3  19354  psrbagsn  19689  musum  25108  ppiub  25120  umgrupgr  26189  umgrislfupgr  26209  usgruspgr  26264  usgrislfuspgr  26270  disjxwwlksn  27014  clwwlknclwwlkdifnum  27093  clwwlknclwwlkdifnumOLD  27095  konigsbergssiedgw  27394  dlwwlknonclwlknonf1olem2  27517  omssubadd  30663  bj-unrab  33220  poimirlem26  33740  poimirlem27  33741  lclkrs2  37323
 Copyright terms: Public domain W3C validator