Theorem csbeq1 3061

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  {cab 2163  [wsbc 2963  ⦋csb 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2964  df-csb 3059

This theorem is referenced by:  csbeq1d  3065  csbeq1a  3067  csbiebg  3100  sbcnestgf  3109  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  csbing  3343  disjnims  3996  sbcbrg  4058  csbopabg  4082  pofun  4313  csbima12g  4990  csbiotag  5210  fvmpts  5595  fvmpt2  5600  mptfvex  5602  elfvmptrab1  5611  fmptcof  5684  fmptcos  5685  fliftfuns  5799  csbriotag  5843  csbov123g  5913  eqerlem  6566  qliftfuns  6619  summodclem2a  11389  zsumdc  11392  fsum3  11395  sumsnf  11417  sumsns  11423  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsumiun  11485  prodsnf  11600  fprodm1s  11609  fprodp1s  11610  prodsns  11611  fprod2dlemstep  11630  fprodcom2fi  11634  pcmptdvds  12343  ctiunctlemf  12439  mulcncflem  14093