![]() |
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 1112 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝑥 ∈ 𝐵))) |
3 | 2 | ralrimiv 3148 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) |
4 | rabss 3969 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) | |
5 | 3, 4 | sylibr 235 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1080 ∈ wcel 2081 ∀wral 3105 {crab 3109 ⊆ wss 3859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rab 3114 df-in 3866 df-ss 3874 |
This theorem is referenced by: suppss2 7715 oemapvali 8993 cantnflem1 8998 harval2 9272 zsupss 12186 ramub1lem1 16191 symggen 18329 efgsfo 18592 ablfacrp 18905 ablfac1eu 18912 pgpfac1lem5 18918 ablfaclem3 18926 nrmr0reg 22041 ptcmplem3 22346 abelthlem2 24703 lgamgulmlem1 25288 neibastop2lem 33317 topmeet 33321 cntotbnd 34606 mapdrvallem2 38312 k0004ss1 39986 liminfvalxr 41606 |
Copyright terms: Public domain | W3C validator |