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  5501  csbopabgALT  5502  pofun  5548  csbima12  6036  csbcog  6253  csbiota  6483  fvmpt2f  6940  fvmpts  6943  fvmpt2i  6950  fvmptex  6954  elfvmptrab1w  6967  elfvmptrab1  6968  fmptcof  7075  fmptcos  7076  fliftfuns  7260  csbriota  7330  riotaeqimp  7341  csbov123  7402  elovmporab1w  7605  elovmporab1  7606  el2mpocsbcl  8026  mposn  8044  mpocurryvald  8211  fvmpocurryd  8212  eqerlem  8670  qliftfuns  8742  boxcutc  8880  iunfi  9244  wdom2d  9486  summolem2a  15639  zsum  15642  fsum  15644  sumsnf  15667  sumsns  15674  fsum2dlem  15694  fsumcom2  15698  fsumshftm  15705  fsum0diag2  15707  fsumrlim  15735  fsumo1  15736  fsumiun  15745  prodmolem2a  15858  prodsn  15886  prodsnf  15888  fprodm1s  15894  fprodp1s  15895  prodsns  15896  fprod2dlem  15904  fprodcom2  15908  pcmptdvds  16823  gsummpt1n0  19898  telgsumfzslem  19921  telgsumfzs  19922  psrass1lem  21889  coe1fzgsumdlem  22246  gsummoncoe1  22251  evl1gsumdlem  22299  madugsum  22586  fiuncmp  23347  elmptrab  23770  ovolfiniun  25446  finiunmbl  25489  volfiniun  25492  iundisj  25493  iundisj2  25494  iunmbl  25498  itgfsum  25772  dvfsumle  25967  dvfsumleOLD  25968  dvfsumabs  25970  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem3  25976  dvfsumlem4  25977  dvfsum2  25982  itgsubstlem  25996  itgsubst  25997  rlimcnp2  26916  fsumdvdscom  27135  fsumdvdsmul  27145  fsumdvdsmulOLD  27147  fsumvma  27164  dchrisumlem2  27441  ifeqeqx  32601  disji2f  32636  disjorsf  32639  disjif2  32640  disjabrex  32641  disjabrexf  32642  disjxpin  32647  iundisjf  32648  iundisj2f  32649  disjunsn  32653  aciunf1lem  32724  funcnv4mpt  32730  iundisjfi  32859  iundisj2fi  32860  fsumiunle  32893  gsummpt2co  33114  itgeq12i  36394  weiunfrlem  36652  weiunpo  36653  weiunso  36654  weiunfr  36655  weiunse  36656  csbttc  36697  finixpnum  37917  poimirlem24  37956  poimirlem26  37958  csbeq12  38470  fsumshftd  39389  cdlemk54  41395  evl1gprodd  42548  idomnnzgmulnz  42564  deg1gprod  42571  mzpsubst  43179  rabdiophlem2  43233  elnn0rabdioph  43234  dvdsrabdioph  43241  fphpd  43247  monotuz  43372  oddcomabszz  43375  fnwe2lem3  43483  flcidc  43601  sumsnd  45460  disjf1  45616  disjrnmpt2  45621  climinf2mpt  46146  climinfmpt  46147  dvnmptdivc  46370  dvmptfprod  46377  fourierdlem103  46641  fourierdlem104  46642  csbafv12g  47571  csbaovg  47614  csbafv212g  47653  fargshiftfva  47877