| 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 1811 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
| 3 | df-ss 3968 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 4 | ss2ab 4062 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
| 5 | 2, 3, 4 | 3imtr4i 292 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
| 6 | df-rab 3437 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
| 7 | df-rab 3437 | . 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
| 8 | 5, 6, 7 | 3sstr4g 4037 | 1 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∀wal 1538 ∈ wcel 2108 {cab 2714 {crab 3436 ⊆ wss 3951 |
| 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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rab 3437 df-ss 3968 |
| This theorem is referenced by: rabssrabd 4083 sess2 5651 hashbcss 17042 dprdss 20049 minveclem4 25466 prmdvdsfi 27150 mumul 27224 sqff1o 27225 rpvmasumlem 27531 disjxwwlkn 29933 clwwlknfi 30064 shatomistici 32380 rabfodom 32524 xpinpreima2 33906 ballotth 34540 bj-unrab 36927 icorempo 37352 lssats 39013 lpssat 39014 lssatle 39016 lssat 39017 atlatmstc 39320 dochspss 41380 unitscyglem4 42199 rmxyelqirrOLD 42922 idomodle 43203 sssmf 46753 |
| Copyright terms: Public domain | W3C validator |