Theorem csbeq1 3052

Description: Analog of dfsbcq 2957 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1	⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Proof of Theorem csbeq1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq 2957	. . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶))
2	1	abbidv 2288	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶})
3		df-csb 3050	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
4		df-csb 3050	. 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}
5	2, 3, 4	3eqtr4g 2228	1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141  {cab 2156  [wsbc 2955  ⦋csb 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956  df-csb 3050

This theorem is referenced by:  csbeq1d  3056  csbeq1a  3058  csbiebg  3091  sbcnestgf  3100  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  csbing  3334  disjnims  3979  sbcbrg  4041  csbopabg  4065  pofun  4295  csbima12g  4970  csbiotag  5189  fvmpts  5572  fvmpt2  5577  mptfvex  5579  elfvmptrab1  5588  fmptcof  5660  fmptcos  5661  fliftfuns  5774  csbriotag  5818  csbov123g  5888  eqerlem  6540  qliftfuns  6593  summodclem2a  11331  zsumdc  11334  fsum3  11337  sumsnf  11359  sumsns  11365  fsum2dlemstep  11384  fisumcom2  11388  fsumshftm  11395  fisum0diag2  11397  fsumiun  11427  prodsnf  11542  fprodm1s  11551  fprodp1s  11552  prodsns  11553  fprod2dlemstep  11572  fprodcom2fi  11576  pcmptdvds  12284  ctiunctlemf  12380  mulcncflem  13343