Theorem csbeq1d 2000

Description: Equality deduction for proper substitution into a class.

Hypothesis

Ref	Expression
csbeq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
csbeq1d	|- (ph -> [_A / x]_C = [_B / x]_C)

Proof of Theorem csbeq1d

Step	Hyp	Ref	Expression
1		csbeq1d.1	. 2 |- (ph -> A = B)
2		csbeq1 1999	. 2 |- (A = B -> [_A / x]_C = [_B / x]_C)
3	1, 2	syl 10	1 |- (ph -> [_A / x]_C = [_B / x]_C)

Syntax hints:   -> wi 3   = wceq 954  [_csb 1997

This theorem is referenced by:  csbnestglem 2031  csbnestg 2032  csbnest1g 2033  csbidmg 2035  csbco3g 2036  fsump1slem 6958  fsum3 6970  fsum4 6971  fsumrev 6975  fsumshft 6977  fsum0diaglem2 7200  fsum0diag 7201  fsum0diag2 7202  fsum0diag4 7204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-sbc 1938  df-csb 1998

Copyright terms: Public domain