![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > csbeq1 | GIF version |
Description: Analog of dfsbcq 2818 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbeq1 | ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 2818 | . . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶)) | |
2 | 1 | abbidv 2197 | . 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}) |
3 | df-csb 2910 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
4 | df-csb 2910 | . 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶} | |
5 | 2, 3, 4 | 3eqtr4g 2139 | 1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ∈ wcel 1434 {cab 2068 [wsbc 2816 ⦋csb 2909 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-sbc 2817 df-csb 2910 |
This theorem is referenced by: csbeq1d 2915 csbeq1a 2917 csbiebg 2946 sbcnestgf 2954 cbvralcsf 2965 cbvrexcsf 2966 cbvreucsf 2967 cbvrabcsf 2968 csbing 3174 sbcbrg 3836 csbopabg 3858 pofun 4069 csbima12g 4710 csbiotag 4919 fvmpts 5276 fvmpt2 5280 mptfvex 5282 fmptcof 5357 fmptcos 5358 fliftfuns 5463 csbriotag 5505 csbov123g 5568 eqerlem 6196 qliftfuns 6249 |
Copyright terms: Public domain | W3C validator |