MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbeq2i Structured version   Unicode version

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
StepHypRef Expression
1 csbeq2i.1 . . . 4  |-  B  =  C
21a1i 11 . . 3  |-  ( T. 
->  B  =  C
)
32csbeq2dv 3843 . 2  |-  ( T. 
->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
43trud 1404 1  |-  [_ A  /  x ]_ B  = 
[_ A  /  x ]_ C
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator