![]() |
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.) Reduce axiom usage. (Revised by Gino Giotto, 15-Oct-2024.) |
Ref | Expression |
---|---|
csbie.1 | ⊢ 𝐴 ∈ V |
csbie.2 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbie | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3895 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
2 | csbie.1 | . . . 4 ⊢ 𝐴 ∈ V | |
3 | csbie.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
4 | 3 | eleq2d 2820 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
5 | 2, 4 | sbcie 3821 | . . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶) |
6 | 5 | abbii 2803 | . 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶} |
7 | abid2 2872 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶 | |
8 | 1, 6, 7 | 3eqtri 2765 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 {cab 2710 Vcvv 3475 [wsbc 3778 ⦋csb 3894 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-sbc 3779 df-csb 3895 |
This theorem is referenced by: pofun 5607 eqerlem 8737 mptnn0fsuppd 13963 fsum 15666 fsumcnv 15719 fsumshftm 15727 fsum0diag2 15729 fprod 15885 fprodcnv 15927 bpolyval 15993 ruclem1 16174 odfval 19400 odval 19402 psrass1lemOLD 21493 psrass1lem 21496 selvval 21681 mamufval 21887 pm2mpval 22297 isibl 25283 dfitg 25287 dvfsumlem2 25544 fsumdvdsmul 26699 precsexlem3 27658 disjxpin 31850 gg-dvfsumlem2 35214 poimirlem1 36537 poimirlem5 36541 poimirlem15 36551 poimirlem16 36552 poimirlem17 36553 poimirlem19 36555 poimirlem20 36556 poimirlem22 36558 poimirlem24 36560 poimirlem28 36564 evlselv 41207 fphpd 41602 monotuz 41728 oddcomabszz 41731 fnwe2val 41839 fnwe2lem1 41840 |
Copyright terms: Public domain | W3C validator |