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 1722 | . 2 ⊢ ∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) |
3 | csbiegf.1 | . . 3 ⊢ (𝐴 ∈ 𝑉 → Ⅎ𝑥𝐶) | |
4 | csbiebt 3553 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑥𝐶) → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | |
5 | 3, 4 | mpdan 702 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) |
6 | 2, 5 | mpbii 223 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1481 = wceq 1483 ∈ wcel 1990 Ⅎwnfc 2751 ⦋csb 3533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-sbc 3436 df-csb 3534 |
This theorem is referenced by: csbief 3558 sbcco3g 3999 csbco3g 4000 fmptcof 6397 fmpt2co 7260 sumsnf 14473 sumsn 14475 prodsn 14692 prodsnf 14694 bpolylem 14779 pcmpt 15596 chfacfpmmulfsupp 20668 elmptrab 21630 dvfsumrlim3 23796 itgsubstlem 23811 itgsubst 23812 ifeqeqx 29361 disjunsn 29407 sbcaltop 32088 unirep 33507 cdleme31so 35667 cdleme31sn 35668 cdleme31sn1 35669 cdleme31se 35670 cdleme31se2 35671 cdleme31sc 35672 cdleme31sde 35673 cdleme31sn2 35677 cdlemeg47rv2 35798 cdlemk41 36208 monotuz 37506 oddcomabszz 37509 |
Copyright terms: Public domain | W3C validator |