![]() |
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 1790 | . 2 ⊢ ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) |
3 | csbiegf.1 | . . 3 ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶) | |
4 | csbiebt 3919 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | |
5 | 3, 4 | mpdan 686 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
6 | 2, 5 | mpbii 232 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1532 = wceq 1534 ∈ wcel 2099 Ⅎwnfc 2878 ⦋csb 3889 |
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-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-v 3471 df-sbc 3775 df-csb 3890 |
This theorem is referenced by: csbief 3924 sbcco3gw 4418 sbcco3g 4423 csbco3g 4424 fmptcof 7133 fmpoco 8094 sumsnf 15713 prodsn 15930 prodsnf 15932 bpolylem 16016 pcmpt 16852 chfacfpmmulfsupp 22752 elmptrab 23718 dvfsumrlim3 25955 itgsubstlem 25970 itgsubst 25971 ifeqeqx 32318 disjunsn 32369 sbcaltop 35513 unirep 37122 cdleme31so 39789 cdleme31sn 39790 cdleme31sn1 39791 cdleme31se 39792 cdleme31se2 39793 cdleme31sc 39794 cdleme31sde 39795 cdleme31sn2 39799 cdlemeg47rv2 39920 cdlemk41 40330 monotuz 42284 oddcomabszz 42287 |
Copyright terms: Public domain | W3C validator |