Theorem rabss 4025

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 3419	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2	1	sseq1i 3966	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵)
3		abss 4017	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵))
4		impexp 456	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵)))
5	4	albii 1852	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵)))
6		df-ral 3082	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵)))
7	5, 6	bitr4i 281	. 2 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))
8	2, 3, 7	3bitri 300	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2146  {cab 2743  ∀wral 3081  {crab 3418   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rab 3419  df-ss 3923

This theorem is used by:  rabssdv  4029  fnsuppres  8193  wemapso2lem  9521  tskwe2  10773  grothac  10830  uzwo3  12983  fsuppmapnn0fiub0  14047  dvdsssfz1  16398  phibndlem  16851  dfphi2  16855  ramval  17090  mgmidsssn0  18756  istopon  23119  ordtrest2lem  23410  filssufilg  24119  cfinufil  24136  blsscls2  24712  nmhmcn  25330  ovolshftlem2  25720  atansssdm  27149  leftf  28099  rightf  28100  umgrres1lem  29718  upgrres1  29721  sspval  31146  ubthlem2  31294  ordtrest2NEWlem  34376  truae  34698  poimirlem30  38358  nnubfi  38459  prnc  38776  supminfrnmpt  46217  supminfxrrnmpt  46243  itgperiod  46753  fourierdlem81  46959  ovnsupge0  47329  smflimlem2  47544