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

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		sbcieg.1	. 2
3	1, 2	sbciegf 3359	1

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