Theorem csbeq1 3831

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  {cab 2715  [wsbc 3711  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712  df-csb 3829

This theorem is referenced by:  csbeq1d  3832  csbeq1a  3842  csbconstg  3847  csbiebg  3861  cbvrabcsfw  3872  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  sbcnestgfw  4349  sbcnestgf  4354  csbun  4369  csbin  4370  csbdif  4455  csbif  4513  disjors  5051  disjxiun  5067  sbcbr123  5124  csbopab  5461  csbopabgALT  5462  pofun  5512  csbima12  5976  csbcog  6189  csbiota  6411  fvmpt2f  6858  fvmpts  6860  fvmpt2i  6867  fvmptex  6871  elfvmptrab1w  6883  elfvmptrab1  6884  fmptcof  6984  fmptcos  6985  fliftfuns  7165  csbriota  7228  riotaeqimp  7239  csbov123  7297  elovmporab1w  7494  elovmporab1  7495  el2mpocsbcl  7896  mposn  7914  mpocurryvald  8057  fvmpocurryd  8058  eqerlem  8490  qliftfuns  8551  boxcutc  8687  iunfi  9037  wdom2d  9269  summolem2a  15355  zsum  15358  fsum  15360  sumsnf  15383  sumsns  15390  fsum2dlem  15410  fsumcom2  15414  fsumshftm  15421  fsum0diag2  15423  fsumrlim  15451  fsumo1  15452  fsumiun  15461  prodmolem2a  15572  prodsn  15600  prodsnf  15602  fprodm1s  15608  fprodp1s  15609  prodsns  15610  fprod2dlem  15618  fprodcom2  15622  pcmptdvds  16523  gsummpt1n0  19481  telgsumfzslem  19504  telgsumfzs  19505  psrass1lemOLD  21053  psrass1lem  21056  coe1fzgsumdlem  21382  gsummoncoe1  21385  evl1gsumdlem  21432  madugsum  21700  fiuncmp  22463  elmptrab  22886  ovolfiniun  24570  finiunmbl  24613  volfiniun  24616  iundisj  24617  iundisj2  24618  iunmbl  24622  itgfsum  24896  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsum2  25103  itgsubstlem  25117  itgsubst  25118  rlimcnp2  26021  fsumdvdscom  26239  fsumdvdsmul  26249  fsumvma  26266  dchrisumlem2  26543  ifeqeqx  30786  disji2f  30817  disjorsf  30820  disjif2  30821  disjabrex  30822  disjabrexf  30823  disjxpin  30828  iundisjf  30829  iundisj2f  30830  disjunsn  30834  aciunf1lem  30901  funcnv4mpt  30908  iundisjfi  31019  iundisj2fi  31020  fsumiunle  31045  gsummpt2co  31210  finixpnum  35689  poimirlem24  35728  poimirlem26  35730  csbeq12  36243  fsumshftd  36893  cdlemk54  38899  mzpsubst  40486  rabdiophlem2  40540  elnn0rabdioph  40541  dvdsrabdioph  40548  fphpd  40554  monotuz  40679  oddcomabszz  40682  fnwe2lem3  40793  flcidc  40915  sumsnd  42458  disjf1  42609  disjrnmpt2  42615  climinf2mpt  43145  climinfmpt  43146  dvnmptdivc  43369  fourierdlem103  43640  fourierdlem104  43641  csbafv12g  44516  csbaovg  44559  csbafv212g  44598  fargshiftfva  44783