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

Theorem rabssab 4040
Description: A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.)
Assertion
Ref Expression
rabssab {𝑥𝐴𝜑} ⊆ {𝑥𝜑}

Proof of Theorem rabssab
StepHypRef Expression
1 df-rab 3419 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 simpr 490 . . 3 ((𝑥𝐴𝜑) → 𝜑)
32ss2abi 4021 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥𝜑}
41, 3eqsstri 3984 1 {𝑥𝐴𝜑} ⊆ {𝑥𝜑}
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wa 401  wcel 2146  {cab 2743  {crab 3418  wss 3906
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737
This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-rab 3419  df-ss 3923
This theorem is used by:  epse  5645  riotasbc  7394  cshwsexa  14887  toponsspwpw  23131  dmtopon  23132  aannenlem2  26545  aalioulem2  26549  ballotlemfmpn  34952  fineqvnttrclse  35596  rencldnfilem  43607  rmxyelqirr  43697  rababg  44360
  Copyright terms: Public domain W3C validator