![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbied | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) Reduce axiom usage. (Revised by Gino Giotto, 15-Oct-2024.) |
Ref | Expression |
---|---|
csbied.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
csbied.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbied | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3895 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
2 | csbied.1 | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
3 | csbied.2 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) | |
4 | 3 | eleq2d 2820 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
5 | 2, 4 | sbcied 3823 | . . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
6 | 5 | alrimiv 1931 | . . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
7 | df-clab 2711 | . . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵) | |
8 | eleq1w 2817 | . . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) | |
9 | 8 | sbcbidv 3837 | . . . . . . . 8 ⊢ (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵)) |
10 | 9 | sbievw 2096 | . . . . . . 7 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵) |
11 | 7, 10 | bitr2i 276 | . . . . . 6 ⊢ ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}) |
12 | 11 | bibi1i 339 | . . . . 5 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) ↔ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) |
13 | 12 | biimpi 215 | . . . 4 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) → (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) |
14 | 6, 13 | sylg 1826 | . . 3 ⊢ (𝜑 → ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) |
15 | dfcleq 2726 | . . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) | |
16 | 14, 15 | sylibr 233 | . 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶) |
17 | 1, 16 | eqtrid 2785 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 = wceq 1542 [wsb 2068 ∈ wcel 2107 {cab 2710 [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: csbied2 3934 rspc2vd 3945 el2mpocl 8072 mposn 8089 cantnfval 9663 fprodeq0 15919 imasval 17457 gsumvalx 18595 efmnd 18751 mulgfval 18952 mulgfvalALT 18953 isga 19155 gexval 19446 telgsumfz 19858 telgsumfz0 19860 telgsum 19862 isirred 20233 znval 21087 psrval 21468 mplval 21548 opsrval 21601 evlsval 21649 evls1fval 21838 evl1fval 21847 scmatval 22006 pmatcollpw3lem 22285 pm2mpval 22297 pm2mpmhmlem2 22321 chfacffsupp 22358 tsmsval2 23634 dvfsumle 25538 dvfsumabs 25540 dvfsumlem1 25543 dvfsum2 25551 itgparts 25564 q1pval 25671 r1pval 25674 rlimcnp2 26471 vmaval 26617 fsumdvdscom 26689 fsumvma 26716 logexprlim 26728 dchrval 26737 dchrisumlema 26991 dchrisumlem2 26993 dchrisumlem3 26994 mulsval 27565 ttgval 28126 ttgvalOLD 28127 finsumvtxdg2sstep 28806 idlsrgval 32617 rprmval 32633 gsummoncoe1fzo 32668 msrval 34529 gg-dvfsumle 35182 poimirlem1 36489 poimirlem2 36490 poimirlem6 36494 poimirlem7 36495 poimirlem10 36498 poimirlem11 36499 poimirlem12 36500 poimirlem23 36511 poimirlem24 36512 fsumshftd 37822 hlhilset 40805 prjspval 41345 mendval 41925 ply1mulgsumlem3 47069 ply1mulgsumlem4 47070 ply1mulgsum 47071 dmatALTval 47081 |
Copyright terms: Public domain | W3C validator |