Theorem csbeq1 3001

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  {cab 2123  [wsbc 2904  ⦋csb 2998

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-sbc 2905  df-csb 2999

This theorem is referenced by:  csbeq1d  3005  csbeq1a  3007  csbiebg  3037  sbcnestgf  3046  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  csbing  3278  disjnims  3916  sbcbrg  3977  csbopabg  4001  pofun  4229  csbima12g  4895  csbiotag  5111  fvmpts  5492  fvmpt2  5497  mptfvex  5499  elfvmptrab1  5508  fmptcof  5580  fmptcos  5581  fliftfuns  5692  csbriotag  5735  csbov123g  5802  eqerlem  6453  qliftfuns  6506  summodclem2a  11143  zsumdc  11146  fsum3  11149  sumsnf  11171  sumsns  11177  fsum2dlemstep  11196  fisumcom2  11200  fsumshftm  11207  fisum0diag2  11209  fsumiun  11239  ctiunctlemf  11940  mulcncflem  12748