Theorem sbcied 3364

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)

Hypotheses

Ref	Expression
sbcied.1
sbcied.2

Assertion

Ref	Expression
sbcied

Distinct variable groups:   ,   ,   ,

Proof of Theorem sbcied

Step	Hyp	Ref	Expression
1		sbcied.1	. 2
2		sbcied.2	. 2
3		nfv 1707	. 2
4		nfvd 1708	. 2
5	1, 2, 3, 4	sbciedf 3363	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  [.wsbc 3327

This theorem is referenced by:  sbcied2  3365  sbc2iedv  3404  sbc3ie  3405  sbcralt  3408  euotd  4753  fmptsnd  6093  riota5f  6282  fpwwe2lem12  9040  fpwwe2lem13  9041  sbcie3s  14676  issubc  15204  gsumvalx  15897  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  issrg  17159  issrng  17499  islmhm  17673  isassa  17964  isphl  18663  istmd  20573  istgp  20576  isnlm  21184  isclm  21564  iscph  21617  iscms  21784  limcfval  22276  sbcies  27381  abfmpeld  27492  abfmpel  27493  isomnd  27691  isorng  27789

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