| 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 3418 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
| 2 | 1 | sseq2i 3968 | . 2 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
| 3 | ssab 4019 | . 2 ⊢ (𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
| 4 | dfss3 3928 | . . . 4 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴) | |
| 5 | 4 | anbi1i 635 | . . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
| 6 | r19.26 3125 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | |
| 7 | df-ral 3080 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
| 8 | 5, 6, 7 | 3bitr2ri 303 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
| 9 | 2, 3, 8 | 3bitri 300 | 1 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∀wal 1561 ∈ wcel 2145 {cab 2743 ∀wral 3079 {crab 3417 ⊆ wss 3907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-tru 1566 df-ex 1803 df-nf 1807 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ral 3080 df-rab 3418 df-ss 3924 |
| This theorem is referenced by: ssrabdv 4029 omssnlim 7865 ordtypelem2 9469 ordtypelem10 9477 card2inf 9505 r0weon 9984 ramtlecl 17050 sscntz 19387 ppttop 23125 epttop 23127 cmpcov2 23508 tgcmp 23519 xkoinjcn 23805 fbssfi 23955 filssufilg 24029 uffixfr 24041 tmdgsum2 24214 symgtgp 24224 ghmcnp 24233 blcls 24624 clsocv 25370 lhop1lem 26133 ressatans 27057 axcontlem3 29225 axcontlem4 29226 ldgenpisyslem3 34472 ldgenpisys 34473 imambfm 34569 fineqvnttrclse 35432 lfuhgr 35481 connpconn 35598 cvmlift2lem11 35676 cvmlift2lem12 35677 bj-rabtr 37427 hbtlem6 43718 usgrexmpl1lem 48641 usgrexmpl2lem 48646 |
| Copyright terms: Public domain | W3C validator |