![]() |
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 3143 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) |
4 | rabss 4034 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 ∈ 𝐵)) | |
5 | 3, 4 | sylibr 233 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 ∈ wcel 2107 ∀wral 3065 {crab 3410 ⊆ wss 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ral 3066 df-rab 3411 df-v 3450 df-in 3922 df-ss 3932 |
This theorem is referenced by: suppss2 8136 oemapvali 9627 cantnflem1 9632 harval2 9940 zsupss 12869 ramub1lem1 16905 symggen 19259 efgsfo 19528 ablfacrp 19852 ablfac1eu 19859 pgpfac1lem5 19865 ablfaclem3 19873 nrmr0reg 23116 ptcmplem3 23421 abelthlem2 25807 lgamgulmlem1 26394 rspectopn 32488 neibastop2lem 34861 topmeet 34865 cntotbnd 36284 mapdrvallem2 40137 onintunirab 41590 nadd2rabex 41731 k0004ss1 42497 liminfvalxr 44098 |
Copyright terms: Public domain | W3C validator |