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 2905 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | 1 | sseq1i 3592 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵) |
3 | abss 3634 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵)) | |
4 | impexp 461 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) | |
5 | 4 | albii 1737 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) |
6 | df-ral 2901 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) | |
7 | 5, 6 | bitr4i 266 | . 2 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) |
8 | 2, 3, 7 | 3bitri 285 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∀wal 1473 ∈ wcel 1977 {cab 2596 ∀wral 2896 {crab 2900 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rab 2905 df-in 3547 df-ss 3554 |
This theorem is referenced by: rabssdv 3645 fnsuppres 7209 wemapso2lem 8340 tskwe2 9474 grothac 9531 uzwo3 11659 fsuppmapnn0fiub0 12655 dvdsssfz1 14878 phibndlem 15313 dfphi2 15317 ramval 15550 mgmidsssn0 17092 istopon 20540 ordtrest2lem 20817 filssufilg 21525 cfinufil 21542 blsscls2 22119 nmhmcn 22728 ovolshftlem2 23085 atansssdm 24460 sspval 26962 ubthlem2 27111 ordtrest2NEWlem 29296 truae 29633 poimirlem30 32609 nnubfi 32716 prnc 33036 itgperiod 38873 fourierdlem81 39080 ovnsupge0 39447 smflimlem2 39658 umgrres1lem 40529 upgrres1 40532 |
Copyright terms: Public domain | W3C validator |