![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > csbeq1 | GIF version |
Description: Analog of dfsbcq 2880 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbeq1 | ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 2880 | . . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶)) | |
2 | 1 | abbidv 2232 | . 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}) |
3 | df-csb 2972 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
4 | df-csb 2972 | . 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶} | |
5 | 2, 3, 4 | 3eqtr4g 2172 | 1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1314 ∈ wcel 1463 {cab 2101 [wsbc 2878 ⦋csb 2971 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-11 1467 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-sbc 2879 df-csb 2972 |
This theorem is referenced by: csbeq1d 2977 csbeq1a 2979 csbiebg 3008 sbcnestgf 3017 cbvralcsf 3028 cbvrexcsf 3029 cbvreucsf 3030 cbvrabcsf 3031 csbing 3249 disjnims 3887 sbcbrg 3944 csbopabg 3966 pofun 4194 csbima12g 4858 csbiotag 5074 fvmpts 5453 fvmpt2 5458 mptfvex 5460 elfvmptrab1 5469 fmptcof 5541 fmptcos 5542 fliftfuns 5653 csbriotag 5696 csbov123g 5763 eqerlem 6414 qliftfuns 6467 summodclem2a 11042 zsumdc 11045 fsum3 11048 sumsnf 11070 sumsns 11076 fsum2dlemstep 11095 fisumcom2 11099 fsumshftm 11106 fisum0diag2 11108 fsumiun 11138 ctiunctlemf 11794 mulcncflem 12576 |
Copyright terms: Public domain | W3C validator |