Theorem csbeq2i 3794

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

Syntax hints:   = wceq 1455   T. wtru 1456   [_csb 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-sbc 3280  df-csb 3376

This theorem is referenced by:  csbnest1g  3802  csbvarg  3804  csbsng  4042  csbprg  4043  csbuni  4240  csbmpt12  4749  csbxp  4935  csbcnv  5037  csbcnvgALT  5038  csbdm  5048  csbres  5127  csbrn  5316  csbfv12  5923  fvmpt2curryd  7044  csbnegg  9898  csbwrdg  12732  matgsum  19511  disjxpin  28247  bj-csbsn  31551  csbopg2  31770  csbpredg  31772  csbwrecsg  31773  csbrecsg  31774  csbrdgg  31775  csboprabg  31776  csbmpt22g  31777  csbfinxpg  31825  poimirlem24  32009  cdleme31so  33991  cdleme31sn  33992  cdleme31sn1  33993  cdleme31se  33994  cdleme31se2  33995  cdleme31sc  33996  cdleme31sde  33997  cdleme31sn2  34001  cdlemkid3N  34545  cdlemkid4  34546  csbunigOLD  37252  csbfv12gALTOLD  37253  csbxpgOLD  37254  csbresgOLD  37256  csbrngOLD  37257  csbima12gALTOLD  37258