Theorem csbeq1 3097

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  {cab 2192  [wsbc 2999  ⦋csb 3094

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-sbc 3000  df-csb 3095

This theorem is referenced by:  csbeq1d  3101  csbeq1a  3103  csbiebg  3137  sbcnestgf  3146  cbvralcsf  3157  cbvrexcsf  3158  cbvreucsf  3159  cbvrabcsf  3160  csbing  3381  disjnims  4038  sbcbrg  4102  csbopabg  4126  pofun  4363  csbima12g  5048  csbiotag  5269  fvmpts  5664  fvmpt2  5670  mptfvex  5672  elfvmptrab1  5681  fmptcof  5754  fmptcos  5755  fliftfuns  5874  csbriotag  5919  csbov123g  5990  elovmporab1w  6154  eqerlem  6658  qliftfuns  6713  summodclem2a  11736  zsumdc  11739  fsum3  11742  sumsnf  11764  sumsns  11770  fsum2dlemstep  11789  fisumcom2  11793  fsumshftm  11800  fisum0diag2  11802  fsumiun  11832  prodsnf  11947  fprodm1s  11956  fprodp1s  11957  prodsns  11958  fprod2dlemstep  11977  fprodcom2fi  11981  pcmptdvds  12712  ctiunctlemf  12853  mulcncflem  15123  fsumdvdsmul  15507