Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssrab | Structured version Visualization version GIF version |
Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.) |
Ref | Expression |
---|---|
ssrab | ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 3144 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | 1 | sseq2i 3993 | . 2 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
3 | ssab 4038 | . 2 ⊢ (𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
4 | dfss3 3953 | . . . 4 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴) | |
5 | 4 | anbi1i 623 | . . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
6 | r19.26 3167 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | |
7 | df-ral 3140 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
8 | 5, 6, 7 | 3bitr2ri 301 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
9 | 2, 3, 8 | 3bitri 298 | 1 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 ∈ wcel 2105 {cab 2796 ∀wral 3135 {crab 3139 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rab 3144 df-in 3940 df-ss 3949 |
This theorem is referenced by: ssrabdv 4047 omssnlim 7583 ordtypelem2 8971 ordtypelem10 8979 card2inf 9007 r0weon 9426 ramtlecl 16324 sscntz 18394 ppttop 21543 epttop 21545 cmpcov2 21926 tgcmp 21937 xkoinjcn 22223 fbssfi 22373 filssufilg 22447 uffixfr 22459 tmdgsum2 22632 symgtgp 22637 ghmcnp 22650 blcls 23043 clsocv 23780 lhop1lem 24537 ressatans 25439 axcontlem3 26679 axcontlem4 26680 ldgenpisyslem3 31323 ldgenpisys 31324 imambfm 31419 lfuhgr 32261 connpconn 32379 cvmlift2lem11 32457 cvmlift2lem12 32458 bj-rabtr 34145 hbtlem6 39607 |
Copyright terms: Public domain | W3C validator |