| 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 3900 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
| 2 | csbie.1 | . . . 4 ⊢ 𝐴 ∈ V | |
| 3 | csbie.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
| 4 | 3 | eleq2d 2827 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
| 5 | 2, 4 | sbcie 3830 | . . 3 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶) |
| 6 | 5 | abbii 2809 | . 2 ⊢ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ 𝑦 ∈ 𝐶} |
| 7 | abid2 2879 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐶} = 𝐶 | |
| 8 | 1, 6, 7 | 3eqtri 2769 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {cab 2714 Vcvv 3480 [wsbc 3788 ⦋csb 3899 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 df-csb 3900 |
| This theorem is referenced by: pofun 5610 eqerlem 8780 mptnn0fsuppd 14039 fsum 15756 fsumcnv 15809 fsumshftm 15817 fsum0diag2 15819 fprod 15977 fprodcnv 16019 bpolyval 16085 ruclem1 16267 odfval 19550 odval 19552 psrass1lem 21952 selvval 22139 mamufval 22396 pm2mpval 22801 isibl 25800 dfitg 25804 dvfsumlem2 26067 dvfsumlem2OLD 26068 fsumdvdsmul 27238 fsumdvdsmulOLD 27240 precsexlem3 28233 disjxpin 32601 poimirlem1 37628 poimirlem5 37632 poimirlem15 37642 poimirlem16 37643 poimirlem17 37644 poimirlem19 37646 poimirlem20 37647 poimirlem22 37649 poimirlem24 37651 poimirlem28 37655 evlselv 42597 fphpd 42827 monotuz 42953 oddcomabszz 42956 fnwe2val 43061 fnwe2lem1 43062 dfswapf2 48967 |
| Copyright terms: Public domain | W3C validator |