Theorem csbeq1 3072

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

Syntax hints:   → wi 4   = wceq 1363   ∈ wcel 2158  {cab 2173  [wsbc 2974  ⦋csb 3069

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 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-sbc 2975  df-csb 3070

This theorem is referenced by:  csbeq1d  3076  csbeq1a  3078  csbiebg  3111  sbcnestgf  3120  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  csbing  3354  disjnims  4007  sbcbrg  4069  csbopabg  4093  pofun  4324  csbima12g  5001  csbiotag  5221  fvmpts  5607  fvmpt2  5612  mptfvex  5614  elfvmptrab1  5623  fmptcof  5696  fmptcos  5697  fliftfuns  5812  csbriotag  5856  csbov123g  5926  eqerlem  6580  qliftfuns  6633  summodclem2a  11403  zsumdc  11406  fsum3  11409  sumsnf  11431  sumsns  11437  fsum2dlemstep  11456  fisumcom2  11460  fsumshftm  11467  fisum0diag2  11469  fsumiun  11499  prodsnf  11614  fprodm1s  11623  fprodp1s  11624  prodsns  11625  fprod2dlemstep  11644  fprodcom2fi  11648  pcmptdvds  12357  ctiunctlemf  12453  mulcncflem  14386