Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbiegf | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
csbiegf.1 | ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶) |
csbiegf.2 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbiegf | ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbiegf.2 | . . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
2 | 1 | ax-gen 1796 | . 2 ⊢ ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) |
3 | csbiegf.1 | . . 3 ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶) | |
4 | csbiebt 3912 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | |
5 | 3, 4 | mpdan 685 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
6 | 2, 5 | mpbii 235 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 = wceq 1537 ∈ wcel 2114 Ⅎwnfc 2961 ⦋csb 3883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-sbc 3773 df-csb 3884 |
This theorem is referenced by: csbief 3917 sbcco3gw 4374 sbcco3g 4379 csbco3g 4380 fmptcof 6892 fmpoco 7790 sumsnf 15099 prodsn 15316 prodsnf 15318 bpolylem 15402 pcmpt 16228 chfacfpmmulfsupp 21471 elmptrab 22435 dvfsumrlim3 24630 itgsubstlem 24645 itgsubst 24646 ifeqeqx 30297 disjunsn 30344 sbcaltop 33442 unirep 35003 cdleme31so 37530 cdleme31sn 37531 cdleme31sn1 37532 cdleme31se 37533 cdleme31se2 37534 cdleme31sc 37535 cdleme31sde 37536 cdleme31sn2 37540 cdlemeg47rv2 37661 cdlemk41 38071 monotuz 39558 oddcomabszz 39561 |
Copyright terms: Public domain | W3C validator |