Theorem csbeq1 2974

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

Syntax hints:   → wi 4   = wceq 1314   ∈ wcel 1463  {cab 2101  [wsbc 2878  ⦋csb 2971

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-sbc 2879  df-csb 2972

This theorem is referenced by:  csbeq1d  2977  csbeq1a  2979  csbiebg  3008  sbcnestgf  3017  cbvralcsf  3028  cbvrexcsf  3029  cbvreucsf  3030  cbvrabcsf  3031  csbing  3249  disjnims  3887  sbcbrg  3944  csbopabg  3966  pofun  4194  csbima12g  4858  csbiotag  5074  fvmpts  5453  fvmpt2  5458  mptfvex  5460  elfvmptrab1  5469  fmptcof  5541  fmptcos  5542  fliftfuns  5653  csbriotag  5696  csbov123g  5763  eqerlem  6414  qliftfuns  6467  summodclem2a  11042  zsumdc  11045  fsum3  11048  sumsnf  11070  sumsns  11076  fsum2dlemstep  11095  fisumcom2  11099  fsumshftm  11106  fisum0diag2  11108  fsumiun  11138  ctiunctlemf  11794  mulcncflem  12576