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

Step	Hyp	Ref	Expression
1		csbeq2i.1	. . . 4
2	1	a1i 11	. . 3
3	2	csbeq2dv 3835	. 2
4	3	trud 1404	1

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