![]() |
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 1797 | . 2 ⊢ ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) |
3 | csbiegf.1 | . . 3 ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶) | |
4 | csbiebt 3857 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | |
5 | 3, 4 | mpdan 686 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
6 | 2, 5 | mpbii 236 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1536 = wceq 1538 ∈ wcel 2111 Ⅎwnfc 2936 ⦋csb 3828 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-v 3443 df-sbc 3721 df-csb 3829 |
This theorem is referenced by: csbief 3862 sbcco3gw 4330 sbcco3g 4335 csbco3g 4336 fmptcof 6869 fmpoco 7773 sumsnf 15091 prodsn 15308 prodsnf 15310 bpolylem 15394 pcmpt 16218 chfacfpmmulfsupp 21468 elmptrab 22432 dvfsumrlim3 24636 itgsubstlem 24651 itgsubst 24652 ifeqeqx 30309 disjunsn 30357 sbcaltop 33555 unirep 35151 cdleme31so 37675 cdleme31sn 37676 cdleme31sn1 37677 cdleme31se 37678 cdleme31se2 37679 cdleme31sc 37680 cdleme31sde 37681 cdleme31sn2 37685 cdlemeg47rv2 37806 cdlemk41 38216 monotuz 39882 oddcomabszz 39885 |
Copyright terms: Public domain | W3C validator |