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

Theorem sbcieg 3360
 Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.)
Hypothesis
Ref Expression
sbcieg.1
Assertion
Ref Expression
sbcieg
Distinct variable groups:   ,   ,

Proof of Theorem sbcieg
StepHypRef Expression
1 nfv 1707 . 2
2 sbcieg.1 . 2
31, 2sbciegf 3359 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  [.wsbc 3327 This theorem is referenced by:  sbcie  3362  ralsng  4064  rexsng  4065  rabsnif  4099  ralrnmpt  6040  fpwwe2lem3  9032  nn1suc  10582  mrcmndind  15997  fgcl  20379  cfinfil  20394  csdfil  20395  supfil  20396  fin1aufil  20433  ifeqeqx  27419  nn0min  27611  2nn0ind  30881  zindbi  30882  trsbcVD  33677  onfrALTlem5VD  33685  bnj1452  34108  cdlemk35s  36663  cdlemk39s  36665  cdlemk42  36667 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-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-v 3111  df-sbc 3328
 Copyright terms: Public domain W3C validator