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

Theorem ssrab 3643
 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 2905 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21sseq2i 3593 . 2 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)})
3 ssab 3635 . 2 (𝐵 ⊆ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
4 dfss3 3558 . . . 4 (𝐵𝐴 ↔ ∀𝑥𝐵 𝑥𝐴)
54anbi1i 727 . . 3 ((𝐵𝐴 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
6 r19.26 3046 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ (∀𝑥𝐵 𝑥𝐴 ∧ ∀𝑥𝐵 𝜑))
7 df-ral 2901 . . 3 (∀𝑥𝐵 (𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)))
85, 6, 73bitr2ri 288 . 2 (∀𝑥(𝑥𝐵 → (𝑥𝐴𝜑)) ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
92, 3, 83bitri 285 1 (𝐵 ⊆ {𝑥𝐴𝜑} ↔ (𝐵𝐴 ∧ ∀𝑥𝐵 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   ∈ wcel 1977  {cab 2596  ∀wral 2896  {crab 2900   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-in 3547  df-ss 3554 This theorem is referenced by:  ssrabdv  3644  omssnlim  6971  ordtypelem2  8307  ordtypelem10  8315  card2inf  8343  r0weon  8718  ramtlecl  15542  sscntz  17582  ppttop  20621  epttop  20623  cmpcov2  21003  tgcmp  21014  xkoinjcn  21300  fbssfi  21451  filssufilg  21525  uffixfr  21537  tmdgsum2  21710  symgtgp  21715  ghmcnp  21728  blcls  22121  clsocv  22857  lhop1lem  23580  ressatans  24461  axcontlem3  25646  axcontlem4  25647  ldgenpisyslem3  29555  ldgenpisys  29556  imambfm  29651  conpcon  30471  cvmlift2lem11  30549  cvmlift2lem12  30550  bj-rabtr  32118  bj-rabtrALTALT  32120  hbtlem6  36718
 Copyright terms: Public domain W3C validator