Theorem csbeq2i 3122

Description: Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)

Hypothesis

Ref	Expression
csbeq2i.1	|- B = C

Assertion

Ref	Expression
csbeq2i	|- [_ A / x ]_ B = [_ A / x ]_ C

Proof of Theorem csbeq2i

Step	Hyp	Ref	Expression
1		csbeq2i.1	. . . 4 |- B = C
2	1	a1i 9	. . 3 |- ( T. -> B = C )
3	2	csbeq2dv 3121	. 2 |- ( T. -> [_ A / x ]_ B = [_ A / x ]_ C )
4	3	mptru 1382	1 |- [_ A / x ]_ B = [_ A / x ]_ C

Syntax hints:   = wceq 1373   T. wtru 1374   [_csb 3095

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 3001  df-csb 3096

This theorem is referenced by:  csbvarg  3123  csbnest1g  3151  csbsng  3696  csbunig  3861  csbxpg  4761  csbcnvg  4867  csbdmg  4878  csbresg  4968  csbrng  5150  csbfv12g  5624  csbnegg  8283  iseqf1olemjpcl  10666  iseqf1olemqpcl  10667  iseqf1olemfvp  10668  seq3f1olemqsum  10671  csbwrdg  11036