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

Theorem ssrab 3829
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 3070 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21sseq2i 3779 . 2 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)})
3 ssab 3821 . 2 (𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
4 dfss3 3741 . . . 4 (𝐵𝐴 ↔ ∀𝑥𝐵 𝑥𝐴)
54anbi1i 610 . . 3 ((𝐵𝐴 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
6 r19.26 3212 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
7 df-ral 3066 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
85, 6, 73bitr2ri 289 . 2 (∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)) ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
92, 3, 83bitri 286 1 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wal 1629  wcel 2145  {cab 2757  wral 3061  {crab 3065  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-in 3730  df-ss 3737
This theorem is referenced by:  ssrabdv  3830  omssnlim  7226  ordtypelem2  8580  ordtypelem10  8588  card2inf  8616  r0weon  9035  ramtlecl  15911  sscntz  17966  ppttop  21032  epttop  21034  cmpcov2  21414  tgcmp  21425  xkoinjcn  21711  fbssfi  21861  filssufilg  21935  uffixfr  21947  tmdgsum2  22120  symgtgp  22125  ghmcnp  22138  blcls  22531  clsocv  23268  lhop1lem  23996  ressatans  24882  axcontlem3  26067  axcontlem4  26068  ldgenpisyslem3  30568  ldgenpisys  30569  imambfm  30664  connpconn  31555  cvmlift2lem11  31633  cvmlift2lem12  31634  bj-rabtr  33258  bj-rabtrALTALT  33260  hbtlem6  38225
  Copyright terms: Public domain W3C validator