![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabss2 | Structured version Visualization version GIF version |
Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
rabss2 | ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.45 622 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
2 | 1 | alimi 1807 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | df-ss 3979 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | ss2ab 4071 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
5 | 2, 3, 4 | 3imtr4i 292 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
6 | df-rab 3433 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
7 | df-rab 3433 | . 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
8 | 5, 6, 7 | 3sstr4g 4040 | 1 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∀wal 1534 ∈ wcel 2105 {cab 2711 {crab 3432 ⊆ wss 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-rab 3433 df-ss 3979 |
This theorem is referenced by: rabssrabd 4092 sess2 5654 hashbcss 17037 dprdss 20063 minveclem4 25479 prmdvdsfi 27164 mumul 27238 sqff1o 27239 rpvmasumlem 27545 disjxwwlkn 29942 clwwlknfi 30073 shatomistici 32389 rabfodom 32532 xpinpreima2 33867 ballotth 34518 bj-unrab 36908 icorempo 37333 lssats 38993 lpssat 38994 lssatle 38996 lssat 38997 atlatmstc 39300 dochspss 41360 unitscyglem4 42179 rmxyelqirrOLD 42898 idomodle 43179 sssmf 46693 |
Copyright terms: Public domain | W3C validator |