Theorem csbeq1 3853

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2740  [wsbc 3742  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbeq1d  3854  csbeq1a  3864  csbconstg  3869  csbiebg  3882  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  sbcnestgfw  4382  sbcnestgf  4387  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  disjors  5090  disjxiun  5104  sbcbr123  5163  csbopab  5538  csbopabw  5539  pofun  5585  csbima12  6079  csbcog  6299  csbiota  6530  fvmpt2f  6991  fvmpts  6994  fvmpt2i  7001  fvmptex  7005  elfvmptrab1w  7018  elfvmptrab1  7019  fmptcof  7127  fmptcos  7128  fliftfuns  7318  csbriota  7388  riotaeqimp  7399  csbov123  7460  elovmporab1w  7664  elovmporab1  7665  el2mpocsbcl  8085  mposn  8103  mpocurryvald  8271  fvmpocurryd  8272  eqerlem  8735  qliftfuns  8807  boxcutc  8951  iunfi  9313  wdom2d  9555  summolem2a  15803  zsum  15806  fsum  15808  sumsnf  15831  sumsns  15838  fsum2dlem  15858  fsumcom2  15862  fsumshftm  15869  fsum0diag2  15871  fsumrlim  15900  fsumo1  15901  fsumiun  15910  prodmolem2a  16025  prodsn  16053  prodsnf  16055  fprodm1s  16061  fprodp1s  16062  prodsns  16063  fprod2dlem  16071  fprodcom2  16075  pcmptdvds  16990  gsummpt1n0  20093  telgsumfzslem  20116  telgsumfzs  20117  psrass1lem  22149  coe1fzgsumdlem  22529  gsummoncoe1  22534  evl1gsumdlem  22582  madugsum  22866  fiuncmp  23630  elmptrab  24054  ovolfiniun  25730  finiunmbl  25773  volfiniun  25776  iundisj  25777  iundisj2  25778  iunmbl  25782  itgfsum  26056  dvfsumle  26250  dvfsumabs  26252  dvfsumlem2  26256  dvfsumlem3  26257  dvfsumlem4  26258  dvfsum2  26263  itgsubstlem  26277  itgsubst  26278  rlimcnp2  27201  fsumdvdscom  27419  fsumdvdsmul  27429  fsumvma  27447  dchrisumlem2  27724  ifeqeqx  33003  disji2f  33037  disjorsf  33040  disjif2  33041  disjabrex  33042  disjabrexf  33043  disjxpin  33048  iundisjf  33049  iundisj2f  33050  disjunsn  33054  aciunf1lem  33122  funcnv4mpt  33128  iundisjfi  33254  iundisj2fi  33255  fsumiunle  33286  gsummpt2co  33475  itgeq12i  36813  weiunfrlem  37070  weiunpo  37071  weiunso  37072  weiunfr  37073  weiunse  37074  csbttc  37115  finixpnum  38346  poimirlem24  38380  poimirlem26  38382  csbeq12  38893  fsumshftd  39812  cdlemk54  41818  evl1gprodd  42970  idomnnzgmulnz  42986  deg1gprod  42993  mzpsubst  43580  rabdiophlem2  43630  elnn0rabdioph  43631  dvdsrabdioph  43638  fphpd  43644  monotuz  43769  oddcomabszz  43772  fnwe2lem3  43880  flcidc  43998  sumsnd  45847  disjf1  46002  disjrnmpt2  46007  climinf2mpt  46529  climinfmpt  46530  dvnmptdivc  46753  dvmptfprod  46760  fourierdlem103  47024  fourierdlem104  47025  csbafv12g  48012  csbaovg  48055  csbafv212g  48094  fargshiftfva  48330