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

Theorem rabss 3712
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 2950 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
21sseq1i 3662 . 2 ({𝑥𝐴𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐵)
3 abss 3704 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥𝐴𝜑) → 𝑥𝐵))
4 impexp 461 . . . 4 (((𝑥𝐴𝜑) → 𝑥𝐵) ↔ (𝑥𝐴 → (𝜑𝑥𝐵)))
54albii 1787 . . 3 (∀𝑥((𝑥𝐴𝜑) → 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝑥𝐵)))
6 df-ral 2946 . . 3 (∀𝑥𝐴 (𝜑𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝑥𝐵)))
75, 6bitr4i 267 . 2 (∀𝑥((𝑥𝐴𝜑) → 𝑥𝐵) ↔ ∀𝑥𝐴 (𝜑𝑥𝐵))
82, 3, 73bitri 286 1 ({𝑥𝐴𝜑} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜑𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521  wcel 2030  {cab 2637  wral 2941  {crab 2945  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-in 3614  df-ss 3621
This theorem is referenced by:  rabssdv  3715  fnsuppres  7367  wemapso2lem  8498  tskwe2  9633  grothac  9690  uzwo3  11821  fsuppmapnn0fiub0  12833  dvdsssfz1  15087  phibndlem  15522  dfphi2  15526  ramval  15759  mgmidsssn0  17316  istopon  20765  ordtrest2lem  21055  filssufilg  21762  cfinufil  21779  blsscls2  22356  nmhmcn  22966  ovolshftlem2  23324  atansssdm  24705  umgrres1lem  26247  upgrres1  26250  sspval  27706  ubthlem2  27855  ordtrest2NEWlem  30096  truae  30434  poimirlem30  33569  nnubfi  33676  prnc  33996  supminfrnmpt  39985  supminfxrrnmpt  40014  itgperiod  40515  fourierdlem81  40722  ovnsupge0  41092  smflimlem2  41301
  Copyright terms: Public domain W3C validator