Theorem csbeq2i 3993

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

Syntax hints:   = wceq 1483   T. wtru 1484   [_csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436  df-csb 3534

This theorem is referenced by:  csbnest1g  4001  csbvarg  4003  csbsng  4243  csbprg  4244  csbopg  4420  csbuni  4466  csbmpt12  5010  csbxp  5200  csbcnv  5306  csbcnvgALT  5307  csbdm  5318  csbres  5399  csbrn  5596  csbfv12  6231  fvmpt2curryd  7397  csbnegg  10278  csbwrdg  13334  matgsum  20243  disjxpin  29401  bj-csbsn  32899  csbpredg  33172  csbwrecsg  33173  csbrecsg  33174  csbrdgg  33175  csboprabg  33176  csbmpt22g  33177  csbfinxpg  33225  poimirlem24  33433  cdleme31so  35667  cdleme31sn  35668  cdleme31sn1  35669  cdleme31se  35670  cdleme31se2  35671  cdleme31sc  35672  cdleme31sde  35673  cdleme31sn2  35677  cdlemkid3N  36221  cdlemkid4  36222  csbunigOLD  39051  csbfv12gALTOLD  39052  csbxpgOLD  39053  csbresgOLD  39055  csbrngOLD  39056  csbima12gALTOLD  39057  climinf2mpt  39946  climinfmpt  39947