![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabss | Structured version Visualization version GIF version |
Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.) |
Ref | Expression |
---|---|
rabss | ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 3434 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | 1 | sseq1i 4024 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵) |
3 | abss 4073 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵)) | |
4 | impexp 450 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) | |
5 | 4 | albii 1816 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) |
6 | df-ral 3060 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) | |
7 | 5, 6 | bitr4i 278 | . 2 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) |
8 | 2, 3, 7 | 3bitri 297 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1535 ∈ wcel 2106 {cab 2712 ∀wral 3059 {crab 3433 ⊆ wss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ral 3060 df-rab 3434 df-ss 3980 |
This theorem is referenced by: rabssdv 4085 fnsuppres 8215 wemapso2lem 9590 tskwe2 10811 grothac 10868 uzwo3 12983 fsuppmapnn0fiub0 14031 dvdsssfz1 16352 phibndlem 16804 dfphi2 16808 ramval 17042 mgmidsssn0 18698 istopon 22934 ordtrest2lem 23227 filssufilg 23935 cfinufil 23952 blsscls2 24533 nmhmcn 25167 ovolshftlem2 25559 atansssdm 26991 leftf 27919 rightf 27920 umgrres1lem 29342 upgrres1 29345 sspval 30752 ubthlem2 30900 ordtrest2NEWlem 33883 truae 34224 poimirlem30 37637 nnubfi 37737 prnc 38054 supminfrnmpt 45395 supminfxrrnmpt 45421 itgperiod 45937 fourierdlem81 46143 ovnsupge0 46513 smflimlem2 46728 |
Copyright terms: Public domain | W3C validator |