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

Theorem csbeq2dv 3835
 Description: Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
csbeq2dv.1
Assertion
Ref Expression
csbeq2dv
Distinct variable group:   ,

Proof of Theorem csbeq2dv
StepHypRef Expression
1 nfv 1707 . 2
2 csbeq2dv.1 . 2
31, 2csbeq2d 3834 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  [_csb 3434 This theorem is referenced by:  csbeq2i  3836  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  offval22  6879  ovmptss  6881  fmpt2co  6883  mpt2sn  6891  mpt2curryd  7017  fvmpt2curryd  7019  cantnffval  8101  fsumcom2  13589  fprodcom2  13788  ruclem1  13964  natfval  15315  fucval  15327  evlfval  15486  mpfrcl  18187  pmatcollpw3lem  19284  fsumcn  21374  fsum2cn  21375  dvmptfsum  22376  ttgval  24178  nbgraopALT  24424  msrfval  28897  bpolylem  29810  bpolyval  29811  rnghmval  32697  dmmpt2ssx2  32926  cdleme31sde  36111  cdlemeg47rv2  36236 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