|   | 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 3436 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
| 2 | 1 | sseq1i 4011 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵) | 
| 3 | abss 4062 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ 𝐵 ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵)) | |
| 4 | impexp 450 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) | |
| 5 | 4 | albii 1818 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝑥 ∈ 𝐵))) | 
| 6 | df-ral 3061 | . . 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 1537 ∈ wcel 2107 {cab 2713 ∀wral 3060 {crab 3435 ⊆ wss 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ral 3061 df-rab 3436 df-ss 3967 | 
| This theorem is referenced by: rabssdv 4074 fnsuppres 8217 wemapso2lem 9593 tskwe2 10814 grothac 10871 uzwo3 12986 fsuppmapnn0fiub0 14035 dvdsssfz1 16356 phibndlem 16808 dfphi2 16812 ramval 17047 mgmidsssn0 18686 istopon 22919 ordtrest2lem 23212 filssufilg 23920 cfinufil 23937 blsscls2 24518 nmhmcn 25154 ovolshftlem2 25546 atansssdm 26977 leftf 27905 rightf 27906 umgrres1lem 29328 upgrres1 29331 sspval 30743 ubthlem2 30891 ordtrest2NEWlem 33922 truae 34245 poimirlem30 37658 nnubfi 37758 prnc 38075 supminfrnmpt 45461 supminfxrrnmpt 45487 itgperiod 46001 fourierdlem81 46207 ovnsupge0 46577 smflimlem2 46792 | 
| Copyright terms: Public domain | W3C validator |