Theorem csbeq1 3083

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  {cab 2179  [wsbc 2985  ⦋csb 3080

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2986  df-csb 3081

This theorem is referenced by:  csbeq1d  3087  csbeq1a  3089  csbiebg  3123  sbcnestgf  3132  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  csbing  3366  disjnims  4021  sbcbrg  4083  csbopabg  4107  pofun  4343  csbima12g  5026  csbiotag  5247  fvmpts  5635  fvmpt2  5641  mptfvex  5643  elfvmptrab1  5652  fmptcof  5725  fmptcos  5726  fliftfuns  5841  csbriotag  5886  csbov123g  5956  elovmporab1w  6119  eqerlem  6618  qliftfuns  6673  summodclem2a  11524  zsumdc  11527  fsum3  11530  sumsnf  11552  sumsns  11558  fsum2dlemstep  11577  fisumcom2  11581  fsumshftm  11588  fisum0diag2  11590  fsumiun  11620  prodsnf  11735  fprodm1s  11744  fprodp1s  11745  prodsns  11746  fprod2dlemstep  11765  fprodcom2fi  11769  pcmptdvds  12483  ctiunctlemf  12595  mulcncflem  14761