![]() |
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 623 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
2 | 1 | alimi 1814 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) |
3 | dfss2 3969 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | ss2ab 4057 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
5 | 2, 3, 4 | 3imtr4i 292 | . 2 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
6 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
7 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
8 | 5, 6, 7 | 3sstr4g 4028 | 1 ⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜑}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∀wal 1540 ∈ wcel 2107 {cab 2710 {crab 3433 ⊆ wss 3949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-rab 3434 df-v 3477 df-in 3956 df-ss 3966 |
This theorem is referenced by: rabssrabd 4082 sess2 5646 hashbcss 16937 dprdss 19899 minveclem4 24949 prmdvdsfi 26611 mumul 26685 sqff1o 26686 rpvmasumlem 26990 disjxwwlkn 29198 clwwlknfi 29329 shatomistici 31645 rabfodom 31774 xpinpreima2 32918 ballotth 33567 bj-unrab 35854 icorempo 36280 lssats 37930 lpssat 37931 lssatle 37933 lssat 37934 atlatmstc 38237 dochspss 40297 rmxyelqirrOLD 41697 idomodle 41986 sssmf 45502 |
Copyright terms: Public domain | W3C validator |