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

Theorem csbeq2i 3836
 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
Assertion
Ref Expression
csbeq2i

Proof of Theorem csbeq2i
StepHypRef Expression
1 csbeq2i.1 . . . 4
21a1i 11 . . 3
32csbeq2dv 3835 . 2
43trud 1404 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395   wtru 1396  [_csb 3434 This theorem is referenced by:  csbnest1g  3845  csbvarg  3848  csbsng  4088  csbprg  4089  csbuni  4277  csbunigOLD  4278  csbmpt12  4786  csbxp  5086  csbxpgOLD  5087  csbcnv  5191  csbcnvgALT  5192  csbdm  5202  csbres  5281  csbresgOLD  5282  csbrn  5473  csbrngOLD  5474  csbfv12  5906  csbfv12gOLD  5907  fvmpt2curryd  7019  csbnegg  9840  csbwrdg  12570  matgsum  18939  disjxpin  27447  csbfv12gALTOLD  33621  csbima12gALTOLD  33622  bj-csbsn  34471  cdleme31so  36105  cdleme31sn  36106  cdleme31sn1  36107  cdleme31se  36108  cdleme31se2  36109  cdleme31sc  36110  cdleme31sde  36111  cdleme31sn2  36115  cdlemkid3N  36659  cdlemkid4  36660 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328  df-csb 3435
 Copyright terms: Public domain W3C validator