![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > csbeq1 | GIF version |
Description: Analog of dfsbcq 2978 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbeq1 | ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 2978 | . . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶)) | |
2 | 1 | abbidv 2306 | . 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}) |
3 | df-csb 3072 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
4 | df-csb 3072 | . 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶} | |
5 | 2, 3, 4 | 3eqtr4g 2246 | 1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1363 ∈ wcel 2159 {cab 2174 [wsbc 2976 ⦋csb 3071 |
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-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2170 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2175 df-cleq 2181 df-clel 2184 df-sbc 2977 df-csb 3072 |
This theorem is referenced by: csbeq1d 3078 csbeq1a 3080 csbiebg 3113 sbcnestgf 3122 cbvralcsf 3133 cbvrexcsf 3134 cbvreucsf 3135 cbvrabcsf 3136 csbing 3356 disjnims 4009 sbcbrg 4071 csbopabg 4095 pofun 4326 csbima12g 5003 csbiotag 5223 fvmpts 5609 fvmpt2 5614 mptfvex 5616 elfvmptrab1 5625 fmptcof 5698 fmptcos 5699 fliftfuns 5814 csbriotag 5858 csbov123g 5928 eqerlem 6583 qliftfuns 6636 summodclem2a 11406 zsumdc 11409 fsum3 11412 sumsnf 11434 sumsns 11440 fsum2dlemstep 11459 fisumcom2 11463 fsumshftm 11470 fisum0diag2 11472 fsumiun 11502 prodsnf 11617 fprodm1s 11626 fprodp1s 11627 prodsns 11628 fprod2dlemstep 11647 fprodcom2fi 11651 pcmptdvds 12360 ctiunctlemf 12456 mulcncflem 14473 |
Copyright terms: Public domain | W3C validator |