![]() |
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 3893 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
2 | csbied.1 | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
3 | csbied.2 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) | |
4 | 3 | eleq2d 2815 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
5 | 2, 4 | sbcied 3822 | . . . . 5 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
6 | 5 | alrimiv 1923 | . . . 4 ⊢ (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
7 | df-clab 2706 | . . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵) | |
8 | eleq1w 2812 | . . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) | |
9 | 8 | sbcbidv 3836 | . . . . . . . 8 ⊢ (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵)) |
10 | 9 | sbievw 2088 | . . . . . . 7 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑧 ∈ 𝐵) |
11 | 7, 10 | bitr2i 276 | . . . . . 6 ⊢ ([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}) |
12 | 11 | bibi1i 338 | . . . . 5 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) ↔ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) |
13 | 12 | biimpi 215 | . . . 4 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶) → (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) |
14 | 6, 13 | sylg 1818 | . . 3 ⊢ (𝜑 → ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) |
15 | dfcleq 2721 | . . 3 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ↔ 𝑧 ∈ 𝐶)) | |
16 | 14, 15 | sylibr 233 | . 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = 𝐶) |
17 | 1, 16 | eqtrid 2780 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∀wal 1532 = wceq 1534 [wsb 2060 ∈ wcel 2099 {cab 2705 [wsbc 3776 ⦋csb 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-sbc 3777 df-csb 3893 |
This theorem is referenced by: csbied2 3932 rspc2vd 3943 el2mpocl 8091 mposn 8108 cantnfval 9692 fprodeq0 15952 imasval 17493 gsumvalx 18636 efmnd 18822 mulgfval 19025 mulgfvalALT 19026 isga 19242 gexval 19533 telgsumfz 19945 telgsumfz0 19947 telgsum 19949 isirred 20358 znval 21465 psrval 21848 mplval 21931 opsrval 21984 evlsval 22032 evls1fval 22238 evl1fval 22247 scmatval 22419 pmatcollpw3lem 22698 pm2mpval 22710 pm2mpmhmlem2 22734 chfacffsupp 22771 tsmsval2 24047 dvfsumle 25967 dvfsumleOLD 25968 dvfsumabs 25970 dvfsumlem1 25973 dvfsum2 25982 itgparts 25995 q1pval 26103 r1pval 26106 rlimcnp2 26911 vmaval 27058 fsumdvdscom 27130 fsumvma 27159 logexprlim 27171 dchrval 27180 dchrisumlema 27434 dchrisumlem2 27436 dchrisumlem3 27437 mulsval 28022 ttgval 28692 ttgvalOLD 28693 finsumvtxdg2sstep 29376 idlsrgval 33227 rprmval 33243 gsummoncoe1fzo 33268 msrval 35148 poimirlem1 37094 poimirlem2 37095 poimirlem6 37099 poimirlem7 37100 poimirlem10 37103 poimirlem11 37104 poimirlem12 37105 poimirlem23 37116 poimirlem24 37117 fsumshftd 38424 hlhilset 41407 isprimroot 41564 prjspval 42027 mendval 42607 ply1mulgsumlem3 47456 ply1mulgsumlem4 47457 ply1mulgsum 47458 dmatALTval 47468 |
Copyright terms: Public domain | W3C validator |