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

Theorem ssrab 3877
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 3105 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21sseq2i 3827 . 2 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)})
3 ssab 3869 . 2 (𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
4 dfss3 3787 . . . 4 (𝐵𝐴 ↔ ∀𝑥𝐵 𝑥𝐴)
54anbi1i 612 . . 3 ((𝐵𝐴 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
6 r19.26 3252 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
7 df-ral 3101 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
85, 6, 73bitr2ri 291 . 2 (∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)) ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
92, 3, 83bitri 288 1 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1635  wcel 2156  {cab 2792  wral 3096  {crab 3100  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rab 3105  df-in 3776  df-ss 3783
This theorem is referenced by:  ssrabdv  3878  omssnlim  7305  ordtypelem2  8659  ordtypelem10  8667  card2inf  8695  r0weon  9114  ramtlecl  15917  sscntz  17956  ppttop  21022  epttop  21024  cmpcov2  21404  tgcmp  21415  xkoinjcn  21701  fbssfi  21851  filssufilg  21925  uffixfr  21937  tmdgsum2  22110  symgtgp  22115  ghmcnp  22128  blcls  22521  clsocv  23258  lhop1lem  23989  ressatans  24874  axcontlem3  26059  axcontlem4  26060  ldgenpisyslem3  30552  ldgenpisys  30553  imambfm  30648  connpconn  31538  cvmlift2lem11  31616  cvmlift2lem12  31617  bj-rabtr  33235  bj-rabtrALTALT  33237  hbtlem6  38197
  Copyright terms: Public domain W3C validator