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

Theorem csbief 3374
 Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
csbief.1
csbief.2
csbief.3
Assertion
Ref Expression
csbief
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem csbief
StepHypRef Expression
1 csbief.1 . 2
2 csbief.2 . . . 4
32a1i 11 . . 3
4 csbief.3 . . 3
53, 4csbiegf 3373 . 2
61, 5ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1452   wcel 1904  wnfc 2599  cvv 3031  csb 3349 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-sbc 3256  df-csb 3350 This theorem is referenced by:  csbie  3375  csbun  3802  csbin  3803  csbif  3922  csbopab  4733  csbopabgALT  4734  csbima12  5191  csbima12gOLD  5192  csbiota  5582  csbriota  6282  csbov123  6342  pcmpt  14916  mpfrcl  18818  iundisj2  22581  iundisj2f  28277  iundisj2fi  28448  csbdif  31796  sbccom2f  32430  csbcog  36312  csbingOLD  37278  csbafv12g  38784  csbaovg  38827
 Copyright terms: Public domain W3C validator