| 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 17048 sscntz 19384 ppttop 23121 epttop 23123 cmpcov2 23504 tgcmp 23515 xkoinjcn 23801 fbssfi 23951 filssufilg 24025 uffixfr 24037 tmdgsum2 24210 symgtgp 24220 ghmcnp 24229 blcls 24620 clsocv 25366 lhop1lem 26129 ressatans 27053 axcontlem3 29221 axcontlem4 29222 ldgenpisyslem3 34467 ldgenpisys 34468 imambfm 34564 fineqvnttrclse 35427 lfuhgr 35476 connpconn 35593 cvmlift2lem11 35671 cvmlift2lem12 35672 bj-rabtr 37422 hbtlem6 43713 usgrexmpl1lem 48642 usgrexmpl2lem 48647 |
| Copyright terms: Public domain | W3C validator |