![]() |
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 1883 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfcvd 2794 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐶) | |
3 | csbied.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
4 | csbied.2 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) | |
5 | 1, 2, 3, 4 | csbiedf 3587 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ⦋csb 3566 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-sbc 3469 df-csb 3567 |
This theorem is referenced by: csbied2 3594 fvmptd 6327 el2mpt2cl 7296 mpt2sn 7313 cantnfval 8603 fprodeq0 14749 imasval 16218 gsumvalx 17317 mulgfval 17589 isga 17770 symgval 17845 gexval 18039 telgsumfz 18433 telgsumfz0 18435 telgsum 18437 isirred 18745 psrval 19410 mplval 19476 opsrval 19522 evlsval 19567 evls1fval 19732 evl1fval 19740 znval 19931 scmatval 20358 pmatcollpw3lem 20636 pm2mpval 20648 pm2mpmhmlem2 20672 chfacffsupp 20709 tsmsval2 21980 dvfsumle 23829 dvfsumabs 23831 dvfsumlem1 23834 dvfsum2 23842 itgparts 23855 q1pval 23958 r1pval 23961 rlimcnp2 24738 vmaval 24884 fsumdvdscom 24956 fsumvma 24983 logexprlim 24995 dchrval 25004 dchrisumlema 25222 dchrisumlem2 25224 dchrisumlem3 25225 ttgval 25800 finsumvtxdg2sstep 26501 rspc2vd 27245 msrval 31561 poimirlem1 33540 poimirlem2 33541 poimirlem6 33545 poimirlem7 33546 poimirlem10 33549 poimirlem11 33550 poimirlem12 33551 poimirlem23 33562 poimirlem24 33563 fsumshftd 34556 hlhilset 37543 mendval 38070 ply1mulgsumlem3 42501 ply1mulgsumlem4 42502 ply1mulgsum 42503 dmatALTval 42514 |
Copyright terms: Public domain | W3C validator |