Theorem csbeq1 3052

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141  {cab 2156  [wsbc 2955  ⦋csb 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956  df-csb 3050

This theorem is referenced by:  csbeq1d  3056  csbeq1a  3058  csbiebg  3091  sbcnestgf  3100  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  csbing  3334  disjnims  3981  sbcbrg  4043  csbopabg  4067  pofun  4297  csbima12g  4972  csbiotag  5191  fvmpts  5574  fvmpt2  5579  mptfvex  5581  elfvmptrab1  5590  fmptcof  5663  fmptcos  5664  fliftfuns  5777  csbriotag  5821  csbov123g  5891  eqerlem  6544  qliftfuns  6597  summodclem2a  11344  zsumdc  11347  fsum3  11350  sumsnf  11372  sumsns  11378  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsumiun  11440  prodsnf  11555  fprodm1s  11564  fprodp1s  11565  prodsns  11566  fprod2dlemstep  11585  fprodcom2fi  11589  pcmptdvds  12297  ctiunctlemf  12393  mulcncflem  13384