![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbief | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
csbief.1 | ⊢ 𝐴 ∈ V |
csbief.2 | ⊢ Ⅎ𝑥𝐶 |
csbief.3 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbief | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbief.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | csbief.2 | . . . 4 ⊢ Ⅎ𝑥𝐶 | |
3 | 2 | a1i 11 | . . 3 ⊢ (𝐴 ∈ V → Ⅎ𝑥𝐶) |
4 | csbief.3 | . . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
5 | 3, 4 | csbiegf 3926 | . 2 ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = 𝐶) |
6 | 1, 5 | ax-mp 5 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2104 Ⅎwnfc 2881 Vcvv 3472 ⦋csb 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-v 3474 df-sbc 3777 df-csb 3893 |
This theorem is referenced by: csbieOLD 3929 cbvrabcsfw 3936 csbun 4437 csbin 4438 csbdif 4526 csbif 4584 csbopab 5554 csbopabgALT 5555 csbima12 6077 csbcog 6295 csbiota 6535 csbriota 7383 csbov123 7453 pcmpt 16829 mpfrcl 21867 iundisj2 25298 iundisj2f 32088 iundisj2fi 32275 csbafv12g 46143 csbaovg 46186 csbafv212g 46225 |
Copyright terms: Public domain | W3C validator |