![]() |
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 GG, 15-Oct-2024.) |
Ref | Expression |
---|---|
csbie.1 | ⊢ 𝐴 ∈ V |
csbie.2 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbie | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3909 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
2 | csbie.1 | . . . 4 ⊢ 𝐴 ∈ V | |
3 | csbie.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
4 | 3 | eleq2d 2825 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
5 | 2, 4 | sbcie 3835 | . . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶) |
6 | 5 | abbii 2807 | . 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶} |
7 | abid2 2877 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶 | |
8 | 1, 6, 7 | 3eqtri 2767 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 {cab 2712 Vcvv 3478 [wsbc 3791 ⦋csb 3908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-sbc 3792 df-csb 3909 |
This theorem is referenced by: pofun 5615 eqerlem 8779 mptnn0fsuppd 14036 fsum 15753 fsumcnv 15806 fsumshftm 15814 fsum0diag2 15816 fprod 15974 fprodcnv 16016 bpolyval 16082 ruclem1 16264 odfval 19565 odval 19567 psrass1lem 21970 selvval 22157 mamufval 22412 pm2mpval 22817 isibl 25815 dfitg 25819 dvfsumlem2 26082 dvfsumlem2OLD 26083 fsumdvdsmul 27253 fsumdvdsmulOLD 27255 precsexlem3 28248 disjxpin 32608 poimirlem1 37608 poimirlem5 37612 poimirlem15 37622 poimirlem16 37623 poimirlem17 37624 poimirlem19 37626 poimirlem20 37627 poimirlem22 37629 poimirlem24 37631 poimirlem28 37635 evlselv 42574 fphpd 42804 monotuz 42930 oddcomabszz 42933 fnwe2val 43038 fnwe2lem1 43039 |
Copyright terms: Public domain | W3C validator |