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 1911 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfcvd 2978 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐶) | |
3 | csbied.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
4 | csbied.2 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) | |
5 | 1, 2, 3, 4 | csbiedf 3912 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ⦋csb 3882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-sbc 3772 df-csb 3883 |
This theorem is referenced by: csbied2 3919 rspc2vd 3931 el2mpocl 7775 mposn 7792 cantnfval 9125 fprodeq0 15323 imasval 16778 gsumvalx 17880 efmnd 18029 mulgfval 18220 mulgfvalALT 18221 isga 18415 gexval 18697 telgsumfz 19104 telgsumfz0 19106 telgsum 19108 isirred 19443 psrval 20136 mplval 20202 opsrval 20249 evlsval 20293 evls1fval 20476 evl1fval 20485 znval 20676 scmatval 21107 pmatcollpw3lem 21385 pm2mpval 21397 pm2mpmhmlem2 21421 chfacffsupp 21458 tsmsval2 22732 dvfsumle 24612 dvfsumabs 24614 dvfsumlem1 24617 dvfsum2 24625 itgparts 24638 q1pval 24741 r1pval 24744 rlimcnp2 25538 vmaval 25684 fsumdvdscom 25756 fsumvma 25783 logexprlim 25795 dchrval 25804 dchrisumlema 26058 dchrisumlem2 26060 dchrisumlem3 26061 ttgval 26655 finsumvtxdg2sstep 27325 msrval 32780 poimirlem1 34887 poimirlem2 34888 poimirlem6 34892 poimirlem7 34893 poimirlem10 34896 poimirlem11 34897 poimirlem12 34898 poimirlem23 34909 poimirlem24 34910 fsumshftd 36082 hlhilset 39064 prjspval 39246 mendval 39776 ply1mulgsumlem3 44436 ply1mulgsumlem4 44437 ply1mulgsum 44438 dmatALTval 44449 |
Copyright terms: Public domain | W3C validator |