Theorem rabss2 3991

Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
rabss2	⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabss2

Step	Hyp	Ref	Expression
1		pm3.45 625	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
2	1	alimi 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3		dfss2 3886	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		ss2ab 3973	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
5	2, 3, 4	3imtr4i 295	. 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)})
6		df-rab 3070	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
7		df-rab 3070	. 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	5, 6, 7	3sstr4g 3946	1 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑})

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1541   ∈ wcel 2110  {cab 2714  {crab 3065   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  rabssrabd  3996  sess2  5520  hashbcss  16557  dprdss  19416  minveclem4  24329  prmdvdsfi  25989  mumul  26063  sqff1o  26064  rpvmasumlem  26368  disjxwwlkn  27997  clwwlknfi  28128  shatomistici  30442  rabfodom  30570  xpinpreima2  31571  ballotth  32216  bj-unrab  34851  icorempo  35259  lssats  36763  lpssat  36764  lssatle  36766  lssat  36767  atlatmstc  37070  dochspss  39129  rmxyelqirr  40435  idomodle  40724  sssmf  43946