![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbied | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
csbied.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
csbied.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbied | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1957 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfcvd 2935 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐶) | |
3 | csbied.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
4 | csbied.2 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) | |
5 | 1, 2, 3, 4 | csbiedf 3772 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∈ wcel 2107 ⦋csb 3751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-sbc 3653 df-csb 3752 |
This theorem is referenced by: csbied2 3779 fvmptd 6548 el2mpt2cl 7531 mpt2sn 7549 cantnfval 8862 fprodeq0 15108 imasval 16557 gsumvalx 17656 mulgfval 17929 isga 18107 symgval 18182 gexval 18377 telgsumfz 18774 telgsumfz0 18776 telgsum 18778 isirred 19086 psrval 19759 mplval 19825 opsrval 19871 evlsval 19915 evls1fval 20080 evl1fval 20088 znval 20279 scmatval 20715 pmatcollpw3lem 20995 pm2mpval 21007 pm2mpmhmlem2 21031 chfacffsupp 21068 tsmsval2 22341 dvfsumle 24221 dvfsumabs 24223 dvfsumlem1 24226 dvfsum2 24234 itgparts 24247 q1pval 24350 r1pval 24353 rlimcnp2 25145 vmaval 25291 fsumdvdscom 25363 fsumvma 25390 logexprlim 25402 dchrval 25411 dchrisumlema 25629 dchrisumlem2 25631 dchrisumlem3 25632 ttgval 26224 finsumvtxdg2sstep 26897 rspc2vd 27673 msrval 32034 poimirlem1 34036 poimirlem2 34037 poimirlem6 34041 poimirlem7 34042 poimirlem10 34045 poimirlem11 34046 poimirlem12 34047 poimirlem23 34058 poimirlem24 34059 fsumshftd 35106 hlhilset 38088 prjspval 38204 mendval 38712 ply1mulgsumlem3 43191 ply1mulgsumlem4 43192 ply1mulgsum 43193 dmatALTval 43204 |
Copyright terms: Public domain | W3C validator |