![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > csbconstg | GIF version |
Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 is not free). csbconstgf 3093 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.) |
Ref | Expression |
---|---|
csbconstg | ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2336 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | 1 | csbconstgf 3093 | 1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ∈ wcel 2164 ⦋csb 3080 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-v 2762 df-sbc 2986 df-csb 3081 |
This theorem is referenced by: sbcel1g 3099 sbceq1g 3100 sbcel2g 3101 sbceq2g 3102 csbidmg 3137 sbcbr12g 4084 sbcbr1g 4085 sbcbr2g 4086 sbcrel 4745 csbcnvg 4846 csbresg 4945 sbcfung 5278 csbfv12g 5592 csbfv2g 5593 elfvmptrab 5653 csbov12g 5957 csbov1g 5958 csbov2g 5959 csbwrdg 10943 |
Copyright terms: Public domain | W3C validator |