Theorem csbeq1 3854

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {cab 2741  [wsbc 3742  ⦋csb 3851

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743  df-csb 3852

This theorem is used by:  csbeq1d  3855  csbeq1a  3865  csbconstg  3870  csbiebg  3883  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbcnestgfw  4382  sbcnestgf  4387  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  disjors  5089  disjxiun  5103  sbcbr123  5163  csbopab  5534  csbopabw  5535  pofun  5581  csbima12  6088  csbcog  6318  csbiota  6551  fvmpt2f  7017  fvmpts  7020  fvmpt2i  7027  fvmptex  7031  elfvmptrab1w  7044  elfvmptrab1  7045  fmptcof  7155  fmptcos  7156  fliftfuns  7345  csbriota  7415  riotaeqimp  7426  csbov123  7487  elovmporab1w  7692  elovmporab1  7693  el2mpocsbcl  8121  mposn  8141  fnwe2lem4  8175  mpocurryvald  8315  fvmpocurryd  8316  eqerlem  8781  qliftfuns  8853  boxcutc  8997  iunfi  9360  wdom2d  9601  summolem2a  15910  zsum  15913  fsum  15915  sumsnf  15938  sumsns  15945  fsum2dlem  15965  fsumcom2  15969  fsumshftm  15976  fsum0diag2  15978  fsumrlim  16007  fsumo1  16008  fsumiun  16017  prodmolem2a  16130  prodsn  16158  prodsnf  16160  fprodm1s  16166  fprodp1s  16167  prodsns  16168  fprod2dlem  16176  fprodcom2  16180  pcmptdvds  17101  gsummpt1n0  20209  telgsumfzslem  20232  telgsumfzs  20233  psrass1lem  22271  coe1fzgsumdlem  22651  gsummoncoe1  22656  evl1gsumdlem  22704  madugsum  22988  fiuncmp  23752  elmptrab  24176  ovolfiniun  25852  finiunmbl  25895  volfiniun  25898  iundisj  25899  iundisj2  25900  iunmbl  25904  itgfsum  26177  dvfsumle  26371  dvfsumabs  26373  dvfsumlem2  26377  dvfsumlem3  26378  dvfsumlem4  26379  dvfsum2  26384  itgsubstlem  26398  itgsubst  26399  rlimcnp2  27324  fsumdvdscom  27542  fsumdvdsmul  27552  fsumvma  27570  dchrisumlem2  27847  ifeqeqx  33210  disji2f  33243  disjorsf  33246  disjif2  33247  disjabrex  33248  disjabrexf  33249  disjxpin  33254  iundisjf  33255  iundisj2f  33256  disjunsn  33260  acunirnmpt2f  33327  aciunf1lem  33328  funcnv4mpt  33334  iundisjfi  33458  iundisj2fi  33459  fsumiunle  33490  gsummpt2co  33679  itgeq12i  37173  weiunfrlem  37430  weiunpo  37431  weiunso  37432  weiunfr  37433  weiunse  37434  csbttc  37475  finixpnum  38720  poimirlem24  38754  poimirlem26  38756  csbeq12  39282  fsumshftd  40201  cdlemk54  42207  evl1gprodd  43359  idomnnzgmulnz  43375  deg1gprod  43382  mzpsubst  43952  rabdiophlem2  44002  elnn0rabdioph  44003  dvdsrabdioph  44010  fphpd  44016  monotuz  44141  oddcomabszz  44144  flcidc  44364  sumsnd  46248  disjf1  46403  disjrnmpt2  46408  climinf2mpt  46929  climinfmpt  46930  dvnmptdivc  47153  dvmptfprod  47160  fourierdlem103  47424  fourierdlem104  47425  csbafv12g  48412  csbaovg  48455  csbafv212g  48494  fargshiftfva  48730