Theorem csbeq2i 3797

Description: Formula-building inference rule 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 11	. . 3 |- ( T. -> B = C )
3	2	csbeq2dv 3796	. 2 |- ( T. -> [_ A / x ]_ B = [_ A / x ]_ C )
4	3	trud 1379	1 |- [_ A / x ]_ B = [_ A / x ]_ C

Syntax hints:   = wceq 1370   T. wtru 1371   [_csb 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3295  df-csb 3397

This theorem is referenced by:  csbnest1g  3806  csbvarg  3809  csbsng  4044  csbuni  4228  csbunigOLD  4229  csbmpt12  4731  csbxp  5027  csbxpgOLD  5028  csbcnv  5132  csbcnvgALT  5133  csbdm  5143  csbres  5222  csbresgOLD  5223  csbrn  5408  csbrngOLD  5409  csbfv12  5835  csbfv12gOLD  5836  fvmpt2curryd  6901  csbnegg  9719  csbwrdg  12376  disjxpin  26082  csbprg  30266  matgsum  31028  csbfv12gALTOLD  31890  csbima12gALTOLD  31891  bj-csbsn  32739  cdleme31so  34362  cdleme31sn  34363  cdleme31sn1  34364  cdleme31se  34365  cdleme31se2  34366  cdleme31sc  34367  cdleme31sde  34368  cdleme31sn2  34372  cdlemkid3N  34916  cdlemkid4  34917