| 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 3146 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
| 3 | ss2rab 4071 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) | |
| 4 | 2, 3 | sylibr 234 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ 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-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: rabssrabd 4083 sess1 5650 suppssov1 8222 suppssov2 8223 suppssfv 8227 cofon1 8710 naddssim 8723 harword 9603 scottex 9925 mrcss 17659 mndpsuppss 18778 ablfac1b 20090 mptscmfsupp0 20925 lspss 20982 dsmmacl 21761 dsmmsubg 21763 dsmmlss 21764 aspss 21897 psdmul 22170 scmatdmat 22521 clsss 23062 lfinpfin 23532 qustgpopn 24128 metss2lem 24524 equivcau 25334 rrxmvallem 25438 ovolsslem 25519 itg2monolem1 25785 lgamucov 27081 sqff1o 27225 musum 27234 madess 27915 cofcut1 27954 cusgrfilem1 29473 clwlknf1oclwwlknlem3 30102 occon 31306 spanss 31367 rmfsupp2 33242 fldgenss 33318 locfinreflem 33839 omsmon 34300 orvclteinc 34478 fin2solem 37613 poimirlem26 37653 poimirlem27 37654 cnambfre 37675 pclssN 39896 2polssN 39917 dihglblem3N 41297 dochss 41367 mapdordlem2 41639 nna4b4nsq 42670 itgoss 43175 nzss 44336 ovnsslelem 46575 gpgusgralem 48011 rmsuppss 48286 scmsuppss 48287 |
| Copyright terms: Public domain | W3C validator |