Theorem csbeq1 3836

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  {cab 2716  [wsbc 3717  ⦋csb 3833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-sbc 3718  df-csb 3834

This theorem is referenced by:  csbeq1d  3837  csbeq1a  3847  csbconstg  3852  csbiebg  3866  cbvrabcsfw  3877  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  sbcnestgfw  4353  sbcnestgf  4358  csbun  4373  csbin  4374  csbdif  4459  csbif  4517  disjors  5056  disjxiun  5072  sbcbr123  5129  csbopab  5469  csbopabgALT  5470  pofun  5522  csbima12  5990  csbcog  6204  csbiota  6430  fvmpt2f  6885  fvmpts  6887  fvmpt2i  6894  fvmptex  6898  elfvmptrab1w  6910  elfvmptrab1  6911  fmptcof  7011  fmptcos  7012  fliftfuns  7194  csbriota  7257  riotaeqimp  7268  csbov123  7326  elovmporab1w  7525  elovmporab1  7526  el2mpocsbcl  7934  mposn  7952  mpocurryvald  8095  fvmpocurryd  8096  eqerlem  8541  qliftfuns  8602  boxcutc  8738  iunfi  9116  wdom2d  9348  summolem2a  15436  zsum  15439  fsum  15441  sumsnf  15464  sumsns  15471  fsum2dlem  15491  fsumcom2  15495  fsumshftm  15502  fsum0diag2  15504  fsumrlim  15532  fsumo1  15533  fsumiun  15542  prodmolem2a  15653  prodsn  15681  prodsnf  15683  fprodm1s  15689  fprodp1s  15690  prodsns  15691  fprod2dlem  15699  fprodcom2  15703  pcmptdvds  16604  gsummpt1n0  19575  telgsumfzslem  19598  telgsumfzs  19599  psrass1lemOLD  21152  psrass1lem  21155  coe1fzgsumdlem  21481  gsummoncoe1  21484  evl1gsumdlem  21531  madugsum  21801  fiuncmp  22564  elmptrab  22987  ovolfiniun  24674  finiunmbl  24717  volfiniun  24720  iundisj  24721  iundisj2  24722  iunmbl  24726  itgfsum  25000  dvfsumle  25194  dvfsumabs  25196  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsum2  25207  itgsubstlem  25221  itgsubst  25222  rlimcnp2  26125  fsumdvdscom  26343  fsumdvdsmul  26353  fsumvma  26370  dchrisumlem2  26647  ifeqeqx  30894  disji2f  30925  disjorsf  30928  disjif2  30929  disjabrex  30930  disjabrexf  30931  disjxpin  30936  iundisjf  30937  iundisj2f  30938  disjunsn  30942  aciunf1lem  31008  funcnv4mpt  31015  iundisjfi  31126  iundisj2fi  31127  fsumiunle  31152  gsummpt2co  31317  finixpnum  35771  poimirlem24  35810  poimirlem26  35812  csbeq12  36325  fsumshftd  36973  cdlemk54  38979  mzpsubst  40577  rabdiophlem2  40631  elnn0rabdioph  40632  dvdsrabdioph  40639  fphpd  40645  monotuz  40770  oddcomabszz  40773  fnwe2lem3  40884  flcidc  41006  sumsnd  42576  disjf1  42727  disjrnmpt2  42733  climinf2mpt  43262  climinfmpt  43263  dvnmptdivc  43486  fourierdlem103  43757  fourierdlem104  43758  csbafv12g  44640  csbaovg  44683  csbafv212g  44722  fargshiftfva  44906