Theorem csbeq1 3060

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

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

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 2963  df-csb 3058

This theorem is referenced by:  csbeq1d  3064  csbeq1a  3066  csbiebg  3099  sbcnestgf  3108  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  csbing  3342  disjnims  3993  sbcbrg  4055  csbopabg  4079  pofun  4310  csbima12g  4986  csbiotag  5206  fvmpts  5591  fvmpt2  5596  mptfvex  5598  elfvmptrab1  5607  fmptcof  5680  fmptcos  5681  fliftfuns  5794  csbriotag  5838  csbov123g  5908  eqerlem  6561  qliftfuns  6614  summodclem2a  11380  zsumdc  11383  fsum3  11386  sumsnf  11408  sumsns  11414  fsum2dlemstep  11433  fisumcom2  11437  fsumshftm  11444  fisum0diag2  11446  fsumiun  11476  prodsnf  11591  fprodm1s  11600  fprodp1s  11601  prodsns  11602  fprod2dlemstep  11621  fprodcom2fi  11625  pcmptdvds  12333  ctiunctlemf  12429  mulcncflem  13872