Theorem csbeq1 3855

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  {cab 2740  [wsbc 3743  ⦋csb 3852

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3744  df-csb 3853

This theorem is used by:  csbeq1d  3856  csbeq1a  3866  csbconstg  3871  csbiebg  3884  cbvrabcsfw  3893  cbvralcsf  3894  cbvreucsf  3896  cbvrabcsf  3897  sbcnestgfw  4385  sbcnestgf  4390  csbun  4405  csbin  4406  csbdif  4485  csbif  4544  disjors  5091  disjxiun  5105  sbcbr123  5164  csbopab  5539  csbopabw  5540  pofun  5586  csbima12  6080  csbcog  6298  csbiota  6529  fvmpt2f  6990  fvmpts  6993  fvmpt2i  7000  fvmptex  7004  elfvmptrab1w  7017  elfvmptrab1  7018  fmptcof  7126  fmptcos  7127  fliftfuns  7312  csbriota  7384  riotaeqimp  7395  csbov123  7456  elovmporab1w  7659  elovmporab1  7660  el2mpocsbcl  8078  mposn  8096  mpocurryvald  8264  fvmpocurryd  8265  eqerlem  8728  qliftfuns  8800  boxcutc  8937  iunfi  9298  wdom2d  9540  summolem2a  15773  zsum  15776  fsum  15778  sumsnf  15801  sumsns  15808  fsum2dlem  15828  fsumcom2  15832  fsumshftm  15839  fsum0diag2  15841  fsumrlim  15870  fsumo1  15871  fsumiun  15880  prodmolem2a  15995  prodsn  16023  prodsnf  16025  fprodm1s  16031  fprodp1s  16032  prodsns  16033  fprod2dlem  16041  fprodcom2  16045  pcmptdvds  16960  gsummpt1n0  20041  telgsumfzslem  20064  telgsumfzs  20065  psrass1lem  22094  coe1fzgsumdlem  22474  gsummoncoe1  22479  evl1gsumdlem  22527  madugsum  22811  fiuncmp  23572  elmptrab  23995  ovolfiniun  25671  finiunmbl  25714  volfiniun  25717  iundisj  25718  iundisj2  25719  iunmbl  25723  itgfsum  25997  dvfsumle  26191  dvfsumabs  26193  dvfsumlem2  26197  dvfsumlem3  26198  dvfsumlem4  26199  dvfsum2  26204  itgsubstlem  26218  itgsubst  26219  rlimcnp2  27142  fsumdvdscom  27360  fsumdvdsmul  27370  fsumvma  27388  dchrisumlem2  27665  ifeqeqx  32899  disji2f  32933  disjorsf  32936  disjif2  32937  disjabrex  32938  disjabrexf  32939  disjxpin  32944  iundisjf  32945  iundisj2f  32946  disjunsn  32950  aciunf1lem  33018  funcnv4mpt  33024  iundisjfi  33152  iundisj2fi  33153  fsumiunle  33184  gsummpt2co  33377  itgeq12i  36746  weiunfrlem  37003  weiunpo  37004  weiunso  37005  weiunfr  37006  weiunse  37007  csbttc  37048  finixpnum  38284  poimirlem24  38323  poimirlem26  38325  csbeq12  38835  fsumshftd  39754  cdlemk54  41760  evl1gprodd  42912  idomnnzgmulnz  42928  deg1gprod  42935  mzpsubst  43507  rabdiophlem2  43557  elnn0rabdioph  43558  dvdsrabdioph  43565  fphpd  43571  monotuz  43696  oddcomabszz  43699  fnwe2lem3  43807  flcidc  43925  sumsnd  45774  disjf1  45929  disjrnmpt2  45934  climinf2mpt  46456  climinfmpt  46457  dvnmptdivc  46680  dvmptfprod  46687  fourierdlem103  46951  fourierdlem104  46952  csbafv12g  47902  csbaovg  47945  csbafv212g  47984  fargshiftfva  48220