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

Theorem ssrab 4003
Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
Assertion
Ref Expression
ssrab (𝐵 ⊆ {𝑥𝐴𝜑} ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab
StepHypRef Expression
1 df-rab 3118 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21sseq2i 3947 . 2 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)})
3 ssab 3992 . 2 (𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
4 dfss3 3906 . . . 4 (𝐵𝐴 ↔ ∀𝑥𝐵 𝑥𝐴)
54anbi1i 626 . . 3 ((𝐵𝐴 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
6 r19.26 3140 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
7 df-ral 3114 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
85, 6, 73bitr2ri 303 . 2 (∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)) ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
92, 3, 83bitri 300 1 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536  wcel 2112  {cab 2779  wral 3109  {crab 3113  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rab 3118  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  ssrabdv  4004  omssnlim  7578  ordtypelem2  8971  ordtypelem10  8979  card2inf  9007  r0weon  9427  ramtlecl  16329  sscntz  18451  ppttop  21615  epttop  21617  cmpcov2  21998  tgcmp  22009  xkoinjcn  22295  fbssfi  22445  filssufilg  22519  uffixfr  22531  tmdgsum2  22704  symgtgp  22714  ghmcnp  22723  blcls  23116  clsocv  23857  lhop1lem  24619  ressatans  25523  axcontlem3  26763  axcontlem4  26764  ldgenpisyslem3  31532  ldgenpisys  31533  imambfm  31628  lfuhgr  32472  connpconn  32590  cvmlift2lem11  32668  cvmlift2lem12  32669  bj-rabtr  34367  hbtlem6  40060
  Copyright terms: Public domain W3C validator