Theorem ss2rab 4068

Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)

Assertion

Ref	Expression
ss2rab	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Proof of Theorem ss2rab

Step	Hyp	Ref	Expression
1		df-rab 3433	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 3433	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	sseq12i 4012	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		ss2ab 4056	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)))
5		df-ral 3062	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
6		imdistan 568	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)))
8	5, 7	bitr2i 275	. 2 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 4, 8	3bitri 296	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   ∈ wcel 2106  {cab 2709  ∀wral 3061  {crab 3432   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  ss2rabdv  4073  ss2rabi  4074  ondomon  10557  eltsms  23636  xrlimcnp  26470  chpssati  31611  lpssat  37878  lssatle  37880  lssat  37881  atlatle  38185  pmaple  38627  diaord  39913  mapdordlem2  40503  rmxyelqirrOLD  41639  ss2rabdf  43834  pimiooltgt  45416  preimageiingt  45426  preimaleiinlt  45427