![]() |
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 1116 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝑥 ∈ 𝐵))) |
3 | 2 | ralrimiv 3134 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) |
4 | rabss 4065 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) | |
5 | 3, 4 | sylibr 233 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 ∈ wcel 2098 ∀wral 3050 {crab 3418 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rab 3419 df-ss 3961 |
This theorem is referenced by: suppss2 8206 oemapvali 9714 cantnflem1 9719 harval2 10027 zsupss 12959 ramub1lem1 17014 symggen 19454 efgsfo 19723 ablfacrp 20052 ablfac1eu 20059 pgpfac1lem5 20065 ablfaclem3 20073 nrmr0reg 23714 ptcmplem3 24019 abelthlem2 26431 lgamgulmlem1 27026 sltonold 28223 rspectopn 33619 neibastop2lem 35995 topmeet 35999 cntotbnd 37420 mapdrvallem2 41268 aks6d1c6lem3 41794 onintunirab 42802 nadd2rabex 42962 k0004ss1 43728 liminfvalxr 45314 |
Copyright terms: Public domain | W3C validator |