Theorem csbeq1 3902

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {cab 2714  [wsbc 3788  ⦋csb 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900

This theorem is referenced by:  csbeq1d  3903  csbeq1a  3913  csbconstg  3918  csbiebg  3931  cbvrabcsfw  3940  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  sbcnestgfw  4421  sbcnestgf  4426  csbun  4441  csbin  4442  csbdif  4524  csbif  4583  disjors  5126  disjxiun  5140  sbcbr123  5197  csbopab  5560  csbopabgALT  5561  pofun  5610  csbima12  6097  csbcog  6317  csbiota  6554  fvmpt2f  7017  fvmpts  7019  fvmpt2i  7026  fvmptex  7030  elfvmptrab1w  7043  elfvmptrab1  7044  fmptcof  7150  fmptcos  7151  fliftfuns  7334  csbriota  7403  riotaeqimp  7414  csbov123  7475  elovmporab1w  7680  elovmporab1  7681  el2mpocsbcl  8110  mposn  8128  mpocurryvald  8295  fvmpocurryd  8296  eqerlem  8780  qliftfuns  8844  boxcutc  8981  iunfi  9383  wdom2d  9620  summolem2a  15751  zsum  15754  fsum  15756  sumsnf  15779  sumsns  15786  fsum2dlem  15806  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  fsumrlim  15847  fsumo1  15848  fsumiun  15857  prodmolem2a  15970  prodsn  15998  prodsnf  16000  fprodm1s  16006  fprodp1s  16007  prodsns  16008  fprod2dlem  16016  fprodcom2  16020  pcmptdvds  16932  gsummpt1n0  19983  telgsumfzslem  20006  telgsumfzs  20007  psrass1lem  21952  coe1fzgsumdlem  22307  gsummoncoe1  22312  evl1gsumdlem  22360  madugsum  22649  fiuncmp  23412  elmptrab  23835  ovolfiniun  25536  finiunmbl  25579  volfiniun  25582  iundisj  25583  iundisj2  25584  iunmbl  25588  itgfsum  25862  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  itgsubstlem  26089  itgsubst  26090  rlimcnp2  27009  fsumdvdscom  27228  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  fsumvma  27257  dchrisumlem2  27534  ifeqeqx  32555  disji2f  32590  disjorsf  32593  disjif2  32594  disjabrex  32595  disjabrexf  32596  disjxpin  32601  iundisjf  32602  iundisj2f  32603  disjunsn  32607  aciunf1lem  32672  funcnv4mpt  32679  iundisjfi  32798  iundisj2fi  32799  fsumiunle  32831  gsummpt2co  33051  itgeq12i  36207  weiunfrlem  36465  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  finixpnum  37612  poimirlem24  37651  poimirlem26  37653  csbeq12  38165  fsumshftd  38953  cdlemk54  40960  evl1gprodd  42118  idomnnzgmulnz  42134  deg1gprod  42141  mzpsubst  42759  rabdiophlem2  42813  elnn0rabdioph  42814  dvdsrabdioph  42821  fphpd  42827  monotuz  42953  oddcomabszz  42956  fnwe2lem3  43064  flcidc  43182  sumsnd  45031  disjf1  45188  disjrnmpt2  45193  climinf2mpt  45729  climinfmpt  45730  dvnmptdivc  45953  dvmptfprod  45960  fourierdlem103  46224  fourierdlem104  46225  csbafv12g  47149  csbaovg  47192  csbafv212g  47231  fargshiftfva  47430