![]() |
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 3149 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
3 | ss2rab 3998 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) | |
4 | 2, 3 | sylibr 237 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 ∀wral 3106 {crab 3110 ⊆ wss 3881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rab 3115 df-v 3443 df-in 3888 df-ss 3898 |
This theorem is referenced by: rabssrabd 4009 sess1 5487 suppssov1 7845 suppssfv 7849 harword 9011 mrcss 16879 ablfac1b 19185 mptscmfsupp0 19692 lspss 19749 dsmmacl 20430 dsmmsubg 20432 dsmmlss 20433 aspss 20563 scmatdmat 21120 clsss 21659 lfinpfin 22129 qustgpopn 22725 metss2lem 23118 equivcau 23904 rrxmvallem 24008 ovolsslem 24088 itg2monolem1 24354 lgamucov 25623 sqff1o 25767 musum 25776 cusgrfilem1 27245 clwlknf1oclwwlknlem3 27868 rmfsupp2 30917 locfinreflem 31193 omsmon 31666 orvclteinc 31843 fin2solem 35043 poimirlem26 35083 poimirlem27 35084 cnambfre 35105 pclssN 37190 2polssN 37211 dihglblem3N 38591 dochss 38661 mapdordlem2 38933 nzss 41021 rmsuppss 44772 mndpsuppss 44773 scmsuppss 44774 |
Copyright terms: Public domain | W3C validator |