Theorem csbeq1 3074

Description: Analog of dfsbcq 2978 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 2978	. . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶))
2	1	abbidv 2306	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶})
3		df-csb 3072	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
4		df-csb 3072	. 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}
5	2, 3, 4	3eqtr4g 2246	1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

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