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

Theorem csbied2 3462
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
csbied2.1
csbied2.2
csbied2.3
Assertion
Ref Expression
csbied2
Distinct variable groups:   ,   ,   ,

Proof of Theorem csbied2
StepHypRef Expression
1 csbied2.1 . 2
2 id 22 . . . 4
3 csbied2.2 . . . 4
42, 3sylan9eqr 2520 . . 3
5 csbied2.3 . . 3
64, 5syldan 470 . 2
71, 6csbied 3461 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  [_csb 3434
This theorem is referenced by:  prdsval  14852  cidfval  15073  monfval  15127  idfuval  15245  isnat  15316  fucco  15331  catcval  15423  xpcval  15446  1stfval  15460  2ndfval  15463  prfval  15468  evlf2  15487  curfval  15492  hofval  15521  ipoval  15784  rngcvalOLD  32769  ringcvalOLD  32815
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-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sbc 3328  df-csb 3435
  Copyright terms: Public domain W3C validator