Theorem csbeq1 3804

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  {cab 2736  [wsbc 3693  ⦋csb 3801

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-sbc 3694  df-csb 3802

This theorem is referenced by:  csbeq1d  3805  csbeq1a  3815  csbiebg  3833  cbvrabcsfw  3842  cbvralcsf  3843  cbvreucsf  3845  cbvrabcsf  3846  sbcnestgfw  4308  sbcnestgf  4313  csbun  4328  csbin  4329  csbif  4470  disjors  5006  disjxiun  5022  sbcbr123  5079  csbopab  5405  csbopabgALT  5406  pofun  5453  csbima12  5912  csbiota  6321  fvmpt2f  6753  fvmpts  6755  fvmpt2i  6762  fvmptex  6766  elfvmptrab1w  6778  elfvmptrab1  6779  fmptcof  6876  fmptcos  6877  fliftfuns  7054  csbriota  7116  riotaeqimp  7127  csbov123  7185  elovmporab1w  7381  elovmporab1  7382  el2mpocsbcl  7778  mposn  7796  mpocurryvald  7939  fvmpocurryd  7940  eqerlem  8326  qliftfuns  8387  boxcutc  8516  iunfi  8830  wdom2d  9062  summolem2a  15105  zsum  15108  fsum  15110  sumsnf  15132  sumsns  15138  fsum2dlem  15158  fsumcom2  15162  fsumshftm  15169  fsum0diag2  15171  fsumrlim  15199  fsumo1  15200  fsumiun  15209  prodmolem2a  15321  prodsn  15349  prodsnf  15351  fprodm1s  15357  fprodp1s  15358  prodsns  15359  fprod2dlem  15367  fprodcom2  15371  pcmptdvds  16270  gsummpt1n0  19138  telgsumfzslem  19161  telgsumfzs  19162  psrass1lemOLD  20687  psrass1lem  20690  coe1fzgsumdlem  21010  gsummoncoe1  21013  evl1gsumdlem  21060  madugsum  21328  fiuncmp  22089  elmptrab  22512  ovolfiniun  24186  finiunmbl  24229  volfiniun  24232  iundisj  24233  iundisj2  24234  iunmbl  24238  itgfsum  24511  dvfsumle  24705  dvfsumabs  24707  dvfsumlem2  24711  dvfsumlem3  24712  dvfsumlem4  24713  dvfsum2  24718  itgsubstlem  24732  itgsubst  24733  rlimcnp2  25636  fsumdvdscom  25854  fsumdvdsmul  25864  fsumvma  25881  dchrisumlem2  26158  ifeqeqx  30392  disji2f  30423  disjorsf  30426  disjif2  30427  disjabrex  30428  disjabrexf  30429  disjxpin  30434  iundisjf  30435  iundisj2f  30436  disjunsn  30440  aciunf1lem  30508  funcnv4mpt  30515  iundisjfi  30626  iundisj2fi  30627  fsumiunle  30652  gsummpt2co  30819  csbdif  35007  finixpnum  35307  poimirlem24  35346  poimirlem26  35348  csbeq12  35861  fsumshftd  36513  cdlemk54  38519  mzpsubst  40047  rabdiophlem2  40101  elnn0rabdioph  40102  dvdsrabdioph  40109  fphpd  40115  monotuz  40240  oddcomabszz  40243  fnwe2lem3  40354  flcidc  40476  csbcog  40708  sumsnd  42013  disjf1  42164  disjrnmpt2  42170  climinf2mpt  42707  climinfmpt  42708  dvnmptdivc  42931  fourierdlem103  43202  fourierdlem104  43203  csbafv12g  44046  csbaovg  44089  csbafv212g  44128  fargshiftfva  44313