![]() |
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 3097 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | 1 | sseq2i 3888 | . 2 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
3 | ssab 3933 | . 2 ⊢ (𝐵 ⊆ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
4 | dfss3 3849 | . . . 4 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴) | |
5 | 4 | anbi1i 614 | . . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
6 | r19.26 3120 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∀𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | |
7 | df-ral 3093 | . . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
8 | 5, 6, 7 | 3bitr2ri 292 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
9 | 2, 3, 8 | 3bitri 289 | 1 ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∀wal 1505 ∈ wcel 2050 {cab 2758 ∀wral 3088 {crab 3092 ⊆ wss 3831 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rab 3097 df-in 3838 df-ss 3845 |
This theorem is referenced by: ssrabdv 3942 omssnlim 7412 ordtypelem2 8780 ordtypelem10 8788 card2inf 8816 r0weon 9234 ramtlecl 16195 sscntz 18230 ppttop 21322 epttop 21324 cmpcov2 21705 tgcmp 21716 xkoinjcn 22002 fbssfi 22152 filssufilg 22226 uffixfr 22238 tmdgsum2 22411 symgtgp 22416 ghmcnp 22429 blcls 22822 clsocv 23559 lhop1lem 24316 ressatans 25216 axcontlem3 26458 axcontlem4 26459 ldgenpisyslem3 31069 ldgenpisys 31070 imambfm 31165 connpconn 32067 cvmlift2lem11 32145 cvmlift2lem12 32146 bj-rabtr 33743 hbtlem6 39125 |
Copyright terms: Public domain | W3C validator |