Theorem csbeq1 3048

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  {cab 2151  [wsbc 2951  ⦋csb 3045

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-sbc 2952  df-csb 3046

This theorem is referenced by:  csbeq1d  3052  csbeq1a  3054  csbiebg  3087  sbcnestgf  3096  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  csbing  3329  disjnims  3974  sbcbrg  4036  csbopabg  4060  pofun  4290  csbima12g  4965  csbiotag  5181  fvmpts  5564  fvmpt2  5569  mptfvex  5571  elfvmptrab1  5580  fmptcof  5652  fmptcos  5653  fliftfuns  5766  csbriotag  5810  csbov123g  5880  eqerlem  6532  qliftfuns  6585  summodclem2a  11322  zsumdc  11325  fsum3  11328  sumsnf  11350  sumsns  11356  fsum2dlemstep  11375  fisumcom2  11379  fsumshftm  11386  fisum0diag2  11388  fsumiun  11418  prodsnf  11533  fprodm1s  11542  fprodp1s  11543  prodsns  11544  fprod2dlemstep  11563  fprodcom2fi  11567  pcmptdvds  12275  ctiunctlemf  12371  mulcncflem  13230