Theorem csbeq1 3150

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  {cab 2224  [wsbc 3051  ⦋csb 3147

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052  df-csb 3148

This theorem is referenced by:  csbeq1d  3154  csbeq1a  3156  csbiebg  3190  sbcnestgf  3199  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  csbing  3438  ifeqeqxdc  3687  disjnims  4119  sbcbrg  4183  csbopabg  4207  pofun  4455  csbima12g  5146  csbiotag  5368  fvmpts  5780  fvmpt2  5786  mptfvex  5788  elfvmptrab1  5797  fmptcof  5869  fmptcos  5870  fliftfuns  5998  csbriotag  6046  riotaeqimp  6057  csbov123g  6118  elovmporab1w  6284  eqerlem  6832  qliftfuns  6887  summodclem2a  12131  zsumdc  12134  fsum3  12137  sumsnf  12159  sumsns  12165  fsum2dlemstep  12184  fisumcom2  12188  fsumshftm  12195  fisum0diag2  12197  fsumiun  12227  prodsnf  12342  fprodm1s  12351  fprodp1s  12352  prodsns  12353  fprod2dlemstep  12372  fprodcom2fi  12376  pcmptdvds  13107  ctiunctlemf  13312  mulcncflem  15691  fsumdvdsmul  16088