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 1830 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfcvd 2752 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐶) | |
3 | csbied.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
4 | csbied.2 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) | |
5 | 1, 2, 3, 4 | csbiedf 3520 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: csbied2 3527 fvmptd 6197 el2mpt2cl 7138 mpt2sn 7155 cantnfval 8448 fprodeq0 14544 imasval 15994 gsumvalx 17093 mulgfval 17365 isga 17547 symgval 17622 gexval 17816 telgsumfz 18210 telgsumfz0 18212 telgsum 18214 isirred 18522 psrval 19183 mplval 19249 opsrval 19295 evlsval 19340 evls1fval 19505 evl1fval 19513 znval 19702 scmatval 20129 pmatcollpw3lem 20407 pm2mpval 20419 pm2mpmhmlem2 20443 chfacffsupp 20480 tsmsval2 21743 dvfsumle 23588 dvfsumabs 23590 dvfsumlem1 23593 dvfsum2 23601 itgparts 23614 q1pval 23717 r1pval 23720 rlimcnp2 24493 vmaval 24639 fsumdvdscom 24711 fsumvma 24738 logexprlim 24750 dchrval 24759 dchrisumlema 24977 dchrisumlem2 24979 dchrisumlem3 24980 ttgval 25555 msrval 30689 poimirlem1 32580 poimirlem2 32581 poimirlem6 32585 poimirlem7 32586 poimirlem10 32589 poimirlem11 32590 poimirlem12 32591 poimirlem23 32602 poimirlem24 32603 fsumshftd 33255 fsumshftdOLD 33256 hlhilset 36244 mendval 36772 rspc2vd 41437 ply1mulgsumlem3 41970 ply1mulgsumlem4 41971 ply1mulgsum 41972 dmatALTval 41983 |
Copyright terms: Public domain | W3C validator |