![]() |
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 27655 disjxpin 31819 gg-dvfsumlem2 35183 poimirlem1 36489 poimirlem5 36493 poimirlem15 36503 poimirlem16 36504 poimirlem17 36505 poimirlem19 36507 poimirlem20 36508 poimirlem22 36510 poimirlem24 36512 poimirlem28 36516 evlselv 41159 fphpd 41554 monotuz 41680 oddcomabszz 41683 fnwe2val 41791 fnwe2lem1 41792 |
Copyright terms: Public domain | W3C validator |