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

Theorem rabss 4071
Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
Assertion
Ref Expression
rabss ({𝑥𝐴𝜑} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜑𝑥𝐵))
Distinct variable group:   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rabss
StepHypRef Expression
1 df-rab 3436 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21sseq1i 4011 . 2 ({𝑥𝐴𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐵)
3 abss 4062 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥𝐴𝜑) → 𝑥𝐵))
4 impexp 450 . . . 4 (((𝑥𝐴𝜑) → 𝑥𝐵) ↔ (𝑥𝐴 → (𝜑𝑥𝐵)))
54albii 1818 . . 3 (∀𝑥((𝑥𝐴𝜑) → 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝑥𝐵)))
6 df-ral 3061 . . 3 (∀𝑥𝐴 (𝜑𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝑥𝐵)))
75, 6bitr4i 278 . 2 (∀𝑥((𝑥𝐴𝜑) → 𝑥𝐵) ↔ ∀𝑥𝐴 (𝜑𝑥𝐵))
82, 3, 73bitri 297 1 ({𝑥𝐴𝜑} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜑𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1537  wcel 2107  {cab 2713  wral 3060  {crab 3435  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rab 3436  df-ss 3967
This theorem is referenced by:  rabssdv  4074  fnsuppres  8217  wemapso2lem  9593  tskwe2  10814  grothac  10871  uzwo3  12986  fsuppmapnn0fiub0  14035  dvdsssfz1  16356  phibndlem  16808  dfphi2  16812  ramval  17047  mgmidsssn0  18686  istopon  22919  ordtrest2lem  23212  filssufilg  23920  cfinufil  23937  blsscls2  24518  nmhmcn  25154  ovolshftlem2  25546  atansssdm  26977  leftf  27905  rightf  27906  umgrres1lem  29328  upgrres1  29331  sspval  30743  ubthlem2  30891  ordtrest2NEWlem  33922  truae  34245  poimirlem30  37658  nnubfi  37758  prnc  38075  supminfrnmpt  45461  supminfxrrnmpt  45487  itgperiod  46001  fourierdlem81  46207  ovnsupge0  46577  smflimlem2  46792
  Copyright terms: Public domain W3C validator