Theorem ssrab 4036

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

Step	Hyp	Ref	Expression
1		df-rab 3406	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2	1	sseq2i 3976	. 2 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
3		ssab 4027	. 2 ⊢ (𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑)))
4		dfss3 3935	. . . 4 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴)
5	4	anbi1i 624	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))
6		r19.26 3091	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))
7		df-ral 3045	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑)))
8	5, 6, 7	3bitr2ri 300	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))
9	2, 3, 8	3bitri 297	1 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  {cab 2707  ∀wral 3044  {crab 3405   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3406  df-ss 3931

This theorem is referenced by:  ssrabdv  4037  omssnlim  7857  ordtypelem2  9472  ordtypelem10  9480  card2inf  9508  r0weon  9965  ramtlecl  16971  sscntz  19258  ppttop  22894  epttop  22896  cmpcov2  23277  tgcmp  23288  xkoinjcn  23574  fbssfi  23724  filssufilg  23798  uffixfr  23810  tmdgsum2  23983  symgtgp  23993  ghmcnp  24002  blcls  24394  clsocv  25150  lhop1lem  25918  ressatans  26844  axcontlem3  28893  axcontlem4  28894  ldgenpisyslem3  34155  ldgenpisys  34156  imambfm  34253  lfuhgr  35105  connpconn  35222  cvmlift2lem11  35300  cvmlift2lem12  35301  bj-rabtr  36918  hbtlem6  43118  usgrexmpl1lem  48012  usgrexmpl2lem  48017