Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbie | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) |
Ref | Expression |
---|---|
csbie.1 | ⊢ 𝐴 ∈ V |
csbie.2 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbie | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbie.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | csbie.2 | . 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
4 | 1, 2, 3 | csbief 3524 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ⦋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: pofun 4975 eqerlem 7663 mptnn0fsuppd 12660 fsum 14298 fsumcnv 14346 fsumshftm 14355 fsum0diag2 14357 fprod 14510 fprodcnv 14552 bpolyval 14619 ruclem1 14799 odval 17776 psrass1lem 19198 mamufval 20010 pm2mpval 20419 isibl 23338 dfitg 23342 dvfsumlem2 23594 fsumdvdsmul 24721 disjxpin 28783 poimirlem1 32580 poimirlem5 32584 poimirlem15 32594 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 poimirlem22 32601 poimirlem24 32603 poimirlem28 32607 fphpd 36398 monotuz 36524 oddcomabszz 36527 fnwe2val 36637 fnwe2lem1 36638 |
Copyright terms: Public domain | W3C validator |