Theorem sbcie 3362

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)

Hypotheses

Ref	Expression
sbcie.1
sbcie.2

Assertion

Ref	Expression
sbcie

Distinct variable groups:   ,   ,

Proof of Theorem sbcie

Step	Hyp	Ref	Expression
1		sbcie.1	. 2
2		sbcie.2	. . 3
3	2	sbcieg 3360	. 2
4	1, 3	ax-mp 5	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  cvv 3109  [.wsbc 3327

This theorem is referenced by:  tfinds2  6698  findcard2  7780  ac6sfi  7784  ac6num  8880  fpwwe  9045  nn1suc  10582  wrdind  12702  cjth  12936  fprodser  13756  prmind2  14228  joinlem  15641  meetlem  15655  mrcmndind  15997  isghm  16267  islmod  17516  islindf  18847  fgcl  20379  cfinfil  20394  csdfil  20395  supfil  20396  fin1aufil  20433  quotval  22688  soseq  29334  sdclem2  30235  fdc  30238  fdc1  30239  rabren3dioph  30749  2nn0ind  30881  zindbi  30882  onfrALTlem5  33314  bnj62  33773  bnj610  33804  bnj976  33836  bnj106  33926  bnj125  33930  bnj154  33936  bnj155  33937  bnj526  33946  bnj540  33950  bnj591  33969  bnj609  33975  bnj893  33986  bnj1417  34097  lshpkrlem3  34837  hdmap1fval  37524  hdmapfval  37557

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