| Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | ||
| Mirrors > Home > MPE Home > Th. List > rabssdv | Structured version Visualization version GIF version | ||
| Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.) | 
| Ref | Expression | 
|---|---|
| rabssdv.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵) | 
| Ref | Expression | 
|---|---|
| rabssdv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | rabssdv.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝑥 ∈ 𝐵) | |
| 2 | 1 | 3exp 1120 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝑥 ∈ 𝐵))) | 
| 3 | 2 | ralrimiv 3145 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) | 
| 4 | rabss 4072 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) | |
| 5 | 3, 4 | sylibr 234 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ w3a 1087 ∈ wcel 2108 ∀wral 3061 {crab 3436 ⊆ wss 3951 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rab 3437 df-ss 3968 | 
| This theorem is referenced by: suppss2 8225 oemapvali 9724 cantnflem1 9729 harval2 10037 zsupss 12979 ramub1lem1 17064 symggen 19488 efgsfo 19757 ablfacrp 20086 ablfac1eu 20093 pgpfac1lem5 20099 ablfaclem3 20107 nrmr0reg 23757 ptcmplem3 24062 abelthlem2 26476 lgamgulmlem1 27072 sltonold 28283 rspectopn 33866 neibastop2lem 36361 topmeet 36365 weiunse 36469 cntotbnd 37803 mapdrvallem2 41647 aks6d1c6lem3 42173 onintunirab 43239 nadd2rabex 43399 k0004ss1 44164 liminfvalxr 45798 | 
| Copyright terms: Public domain | W3C validator |