Theorem rabss 3969

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

Step	Hyp	Ref	Expression
1		df-rab 3114	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2	1	sseq1i 3916	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵)
3		abss 3961	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵))
4		impexp 451	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵)))
5	4	albii 1801	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵)))
6		df-ral 3110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵)))
7	5, 6	bitr4i 279	. 2 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))
8	2, 3, 7	3bitri 298	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1520   ∈ wcel 2081  {cab 2775  ∀wral 3105  {crab 3109   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rab 3114  df-in 3866  df-ss 3874

This theorem is referenced by:  rabssdv  3972  fnsuppres  7708  wemapso2lem  8862  tskwe2  10041  grothac  10098  uzwo3  12192  fsuppmapnn0fiub0  13211  dvdsssfz1  15501  phibndlem  15936  dfphi2  15940  ramval  16173  mgmidsssn0  17708  istopon  21204  ordtrest2lem  21495  filssufilg  22203  cfinufil  22220  blsscls2  22797  nmhmcn  23407  ovolshftlem2  23794  atansssdm  25192  umgrres1lem  26775  upgrres1  26778  sspval  28191  ubthlem2  28339  ordtrest2NEWlem  30782  truae  31119  poimirlem30  34472  nnubfi  34576  prnc  34896  supminfrnmpt  41280  supminfxrrnmpt  41308  itgperiod  41827  fourierdlem81  42034  ovnsupge0  42401  smflimlem2  42610