Theorem csbeq2i 3844

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 3843	. 2 |- ( T. -> [_ A / x ]_ B = [_ A / x ]_ C )
4	3	trud 1404	1 |- [_ A / x ]_ B = [_ A / x ]_ C

Syntax hints:   = wceq 1395   T. wtru 1396   [_csb 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328  df-csb 3431

This theorem is referenced by:  csbnest1g  3852  csbvarg  3855  csbsng  4090  csbprg  4091  csbuni  4279  csbunigOLD  4280  csbmpt12  4790  csbxp  5090  csbxpgOLD  5091  csbcnv  5196  csbcnvgALT  5197  csbdm  5207  csbres  5286  csbresgOLD  5287  csbrn  5474  csbrngOLD  5475  csbfv12  5907  fvmpt2curryd  7018  csbnegg  9836  csbwrdg  12577  matgsum  19065  disjxpin  27584  csbfv12gALTOLD  33722  csbima12gALTOLD  33723  bj-csbsn  34572  cdleme31so  36206  cdleme31sn  36207  cdleme31sn1  36208  cdleme31se  36209  cdleme31se2  36210  cdleme31sc  36211  cdleme31sde  36212  cdleme31sn2  36216  cdlemkid3N  36760  cdlemkid4  36761