Theorem csbeq1 3851

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  {cab 2708  [wsbc 3739  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3740  df-csb 3849

This theorem is referenced by:  csbeq1d  3852  csbeq1a  3862  csbconstg  3867  csbiebg  3880  cbvrabcsfw  3889  cbvralcsf  3890  cbvreucsf  3892  cbvrabcsf  3893  sbcnestgfw  4369  sbcnestgf  4374  csbun  4389  csbin  4390  csbdif  4472  csbif  4531  disjors  5072  disjxiun  5086  sbcbr123  5143  csbopab  5493  csbopabgALT  5494  pofun  5540  csbima12  6025  csbcog  6240  csbiota  6470  fvmpt2f  6925  fvmpts  6927  fvmpt2i  6934  fvmptex  6938  elfvmptrab1w  6951  elfvmptrab1  6952  fmptcof  7058  fmptcos  7059  fliftfuns  7243  csbriota  7313  riotaeqimp  7324  csbov123  7385  elovmporab1w  7588  elovmporab1  7589  el2mpocsbcl  8010  mposn  8028  mpocurryvald  8195  fvmpocurryd  8196  eqerlem  8652  qliftfuns  8723  boxcutc  8860  iunfi  9222  wdom2d  9461  summolem2a  15614  zsum  15617  fsum  15619  sumsnf  15642  sumsns  15649  fsum2dlem  15669  fsumcom2  15673  fsumshftm  15680  fsum0diag2  15682  fsumrlim  15710  fsumo1  15711  fsumiun  15720  prodmolem2a  15833  prodsn  15861  prodsnf  15863  fprodm1s  15869  fprodp1s  15870  prodsns  15871  fprod2dlem  15879  fprodcom2  15883  pcmptdvds  16798  gsummpt1n0  19870  telgsumfzslem  19893  telgsumfzs  19894  psrass1lem  21862  coe1fzgsumdlem  22211  gsummoncoe1  22216  evl1gsumdlem  22264  madugsum  22551  fiuncmp  23312  elmptrab  23735  ovolfiniun  25422  finiunmbl  25465  volfiniun  25468  iundisj  25469  iundisj2  25470  iunmbl  25474  itgfsum  25748  dvfsumle  25946  dvfsumleOLD  25947  dvfsumabs  25949  dvfsumlem2  25953  dvfsumlem2OLD  25954  dvfsumlem3  25955  dvfsumlem4  25956  dvfsum2  25961  itgsubstlem  25975  itgsubst  25976  rlimcnp2  26896  fsumdvdscom  27115  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  fsumvma  27144  dchrisumlem2  27421  ifeqeqx  32512  disji2f  32547  disjorsf  32550  disjif2  32551  disjabrex  32552  disjabrexf  32553  disjxpin  32558  iundisjf  32559  iundisj2f  32560  disjunsn  32564  aciunf1lem  32634  funcnv4mpt  32641  iundisjfi  32768  iundisj2fi  32769  fsumiunle  32802  gsummpt2co  33018  itgeq12i  36219  weiunfrlem  36477  weiunpo  36478  weiunso  36479  weiunfr  36480  weiunse  36481  finixpnum  37624  poimirlem24  37663  poimirlem26  37665  csbeq12  38177  fsumshftd  38970  cdlemk54  40976  evl1gprodd  42129  idomnnzgmulnz  42145  deg1gprod  42152  mzpsubst  42760  rabdiophlem2  42814  elnn0rabdioph  42815  dvdsrabdioph  42822  fphpd  42828  monotuz  42953  oddcomabszz  42956  fnwe2lem3  43064  flcidc  43182  sumsnd  45042  disjf1  45199  disjrnmpt2  45204  climinf2mpt  45731  climinfmpt  45732  dvnmptdivc  45955  dvmptfprod  45962  fourierdlem103  46226  fourierdlem104  46227  csbafv12g  47147  csbaovg  47190  csbafv212g  47229  fargshiftfva  47453