Theorem rabss2 4025

Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid axioms. (Revised by TM, 1-Feb-2026.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabss2

Step	Hyp	Ref	Expression
1		ssel 3925	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 623	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	ss2abdv 4013	. 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)})
4		df-rab 3414	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
5		df-rab 3414	. 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
6	3, 4, 5	3sstr4g 3984	1 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  {cab 2739  {crab 3413   ⊆ wss 3899

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916

This theorem is used by:  rabssrabd  4031  sess2  5617  hashbcss  17175  dprdss  20238  minveclem4  25746  prmdvdsfi  27427  mumul  27501  sqff1o  27502  rpvmasumlem  27807  disjxwwlkn  30495  clwwlknfi  30629  shatomistici  32956  rabfodom  33094  xpinpreima2  34532  ballotth  35163  bj-unrab  37819  icorempo  38254  lssats  40049  lpssat  40050  lssatle  40052  lssat  40053  atlatmstc  40356  dochspss  42415  unitscyglem4  43228  idomodle  44177  sssmf  47717