Theorem csbeq1 3849

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {cab 2738  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbeq1d  3850  csbeq1a  3860  csbconstg  3865  csbiebg  3878  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbcnestgfw  4378  sbcnestgf  4383  csbun  4398  csbin  4399  csbdif  4480  csbif  4539  disjors  5085  disjxiun  5099  sbcbr123  5159  csbopab  5529  csbopabw  5530  pofun  5576  csbima12  6075  csbcog  6300  csbiota  6531  fvmpt2f  6994  fvmpts  6997  fvmpt2i  7004  fvmptex  7008  elfvmptrab1w  7021  elfvmptrab1  7022  fmptcof  7131  fmptcos  7132  fliftfuns  7322  csbriota  7392  riotaeqimp  7403  csbov123  7464  elovmporab1w  7668  elovmporab1  7669  el2mpocsbcl  8096  mposn  8114  fnwe2lem4  8148  mpocurryvald  8287  fvmpocurryd  8288  eqerlem  8753  qliftfuns  8825  boxcutc  8969  iunfi  9332  wdom2d  9574  summolem2a  15881  zsum  15884  fsum  15886  sumsnf  15909  sumsns  15916  fsum2dlem  15936  fsumcom2  15940  fsumshftm  15947  fsum0diag2  15949  fsumrlim  15978  fsumo1  15979  fsumiun  15988  prodmolem2a  16101  prodsn  16129  prodsnf  16131  fprodm1s  16137  fprodp1s  16138  prodsns  16139  fprod2dlem  16147  fprodcom2  16151  pcmptdvds  17072  gsummpt1n0  20179  telgsumfzslem  20202  telgsumfzs  20203  psrass1lem  22241  coe1fzgsumdlem  22621  gsummoncoe1  22626  evl1gsumdlem  22674  madugsum  22958  fiuncmp  23722  elmptrab  24146  ovolfiniun  25822  finiunmbl  25865  volfiniun  25868  iundisj  25869  iundisj2  25870  iunmbl  25874  itgfsum  26147  dvfsumle  26341  dvfsumabs  26343  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsum2  26354  itgsubstlem  26368  itgsubst  26369  rlimcnp2  27294  fsumdvdscom  27512  fsumdvdsmul  27522  fsumvma  27540  dchrisumlem2  27817  ifeqeqx  33180  disji2f  33213  disjorsf  33216  disjif2  33217  disjabrex  33218  disjabrexf  33219  disjxpin  33224  iundisjf  33225  iundisj2f  33226  disjunsn  33230  aciunf1lem  33298  funcnv4mpt  33304  iundisjfi  33430  iundisj2fi  33431  fsumiunle  33462  gsummpt2co  33651  itgeq12i  37037  weiunfrlem  37294  weiunpo  37295  weiunso  37296  weiunfr  37297  weiunse  37298  csbttc  37339  finixpnum  38571  poimirlem24  38605  poimirlem26  38607  csbeq12  39133  fsumshftd  40052  cdlemk54  42058  evl1gprodd  43210  idomnnzgmulnz  43226  deg1gprod  43233  mzpsubst  43802  rabdiophlem2  43852  elnn0rabdioph  43853  dvdsrabdioph  43860  fphpd  43866  monotuz  43991  oddcomabszz  43994  flcidc  44215  sumsnd  46086  disjf1  46241  disjrnmpt2  46246  climinf2mpt  46767  climinfmpt  46768  dvnmptdivc  46991  dvmptfprod  46998  fourierdlem103  47262  fourierdlem104  47263  csbafv12g  48250  csbaovg  48293  csbafv212g  48332  fargshiftfva  48568