Theorem csbeq1a 2002

Description: Equality theorem for proper substitution into a class.

Assertion

Ref	Expression
csbeq1a	|- (x = A -> B = [_A / x]_B)

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbeq1 1999	. 2 |- (x = A -> [_x / x]_B = [_A / x]_B)
2		csbid 2001	. 2 |- [_x / x]_B = B
3	1, 2	syl5eqr 1518	1 |- (x = A -> B = [_A / x]_B)

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

This theorem is referenced by:  csbieb 2026  csbie2t 2029  csbnestglem 2031  csbnest1g 2033  uniiunlem 2128  sbcbrg 2657  csbima12g 3405  csbfv12g 3733  fvopab4gf 3772  fvopab4sf 3773  fvopabs 3783  csboprg 3977  oprabval2gf 4017  csbopeq1a 4102  csbnegg 5344  fsum1slem 6954  fsump1slem 6958  isumnn0nna 7151  infcvgaux1 7162  fsum0diaglem2 7200  fsum0diag 7201  fsum0diag2 7202

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