Theorem csbeq1 3841

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3729  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbeq1d  3842  csbeq1a  3852  csbconstg  3857  csbiebg  3870  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  sbcnestgfw  4362  sbcnestgf  4367  csbun  4382  csbin  4383  csbdif  4466  csbif  4525  disjors  5069  disjxiun  5083  sbcbr123  5140  csbopab  5510  csbopabgALT  5511  pofun  5557  csbima12  6045  csbcog  6262  csbiota  6492  fvmpt2f  6949  fvmpts  6952  fvmpt2i  6959  fvmptex  6963  elfvmptrab1w  6976  elfvmptrab1  6977  fmptcof  7084  fmptcos  7085  fliftfuns  7269  csbriota  7339  riotaeqimp  7350  csbov123  7411  elovmporab1w  7614  elovmporab1  7615  el2mpocsbcl  8035  mposn  8053  mpocurryvald  8220  fvmpocurryd  8221  eqerlem  8679  qliftfuns  8751  boxcutc  8889  iunfi  9253  wdom2d  9495  summolem2a  15677  zsum  15680  fsum  15682  sumsnf  15705  sumsns  15712  fsum2dlem  15732  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsumrlim  15774  fsumo1  15775  fsumiun  15784  prodmolem2a  15899  prodsn  15927  prodsnf  15929  fprodm1s  15935  fprodp1s  15936  prodsns  15937  fprod2dlem  15945  fprodcom2  15949  pcmptdvds  16865  gsummpt1n0  19940  telgsumfzslem  19963  telgsumfzs  19964  psrass1lem  21912  coe1fzgsumdlem  22268  gsummoncoe1  22273  evl1gsumdlem  22321  madugsum  22608  fiuncmp  23369  elmptrab  23792  ovolfiniun  25468  finiunmbl  25511  volfiniun  25514  iundisj  25515  iundisj2  25516  iunmbl  25520  itgfsum  25794  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  itgsubstlem  26015  itgsubst  26016  rlimcnp2  26930  fsumdvdscom  27148  fsumdvdsmul  27158  fsumvma  27176  dchrisumlem2  27453  ifeqeqx  32612  disji2f  32647  disjorsf  32650  disjif2  32651  disjabrex  32652  disjabrexf  32653  disjxpin  32658  iundisjf  32659  iundisj2f  32660  disjunsn  32664  aciunf1lem  32735  funcnv4mpt  32741  iundisjfi  32869  iundisj2fi  32870  fsumiunle  32902  gsummpt2co  33109  itgeq12i  36388  weiunfrlem  36646  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  csbttc  36691  finixpnum  37926  poimirlem24  37965  poimirlem26  37967  csbeq12  38479  fsumshftd  39398  cdlemk54  41404  evl1gprodd  42556  idomnnzgmulnz  42572  deg1gprod  42579  mzpsubst  43180  rabdiophlem2  43230  elnn0rabdioph  43231  dvdsrabdioph  43238  fphpd  43244  monotuz  43369  oddcomabszz  43372  fnwe2lem3  43480  flcidc  43598  sumsnd  45457  disjf1  45613  disjrnmpt2  45618  climinf2mpt  46142  climinfmpt  46143  dvnmptdivc  46366  dvmptfprod  46373  fourierdlem103  46637  fourierdlem104  46638  csbafv12g  47579  csbaovg  47622  csbafv212g  47661  fargshiftfva  47897