![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss2rabdv | Structured version Visualization version GIF version |
Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) |
Ref | Expression |
---|---|
ss2rabdv.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ss2rabdv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2rabdv.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
2 | 1 | ralrimiva 3143 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
3 | ss2rab 4080 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) | |
4 | 2, 3 | sylibr 234 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2105 ∀wral 3058 {crab 3432 ⊆ wss 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rab 3433 df-ss 3979 |
This theorem is referenced by: rabssrabd 4092 sess1 5653 suppssov1 8220 suppssov2 8221 suppssfv 8225 cofon1 8708 naddssim 8721 harword 9600 scottex 9922 mrcss 17660 mndpsuppss 18790 ablfac1b 20104 mptscmfsupp0 20941 lspss 20999 dsmmacl 21778 dsmmsubg 21780 dsmmlss 21781 aspss 21914 psdmul 22187 scmatdmat 22536 clsss 23077 lfinpfin 23547 qustgpopn 24143 metss2lem 24539 equivcau 25347 rrxmvallem 25451 ovolsslem 25532 itg2monolem1 25799 lgamucov 27095 sqff1o 27239 musum 27248 madess 27929 cofcut1 27968 cusgrfilem1 29487 clwlknf1oclwwlknlem3 30111 occon 31315 spanss 31376 rmfsupp2 33227 fldgenss 33297 locfinreflem 33800 omsmon 34279 orvclteinc 34456 fin2solem 37592 poimirlem26 37632 poimirlem27 37633 cnambfre 37654 pclssN 39876 2polssN 39897 dihglblem3N 41277 dochss 41347 mapdordlem2 41619 nna4b4nsq 42646 itgoss 43151 nzss 44312 ovnsslelem 46515 gpgusgralem 47945 rmsuppss 48214 scmsuppss 48215 |
Copyright terms: Public domain | W3C validator |