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

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
StepHypRef Expression
1 sbcied.1 . 2
2 sbcied.2 . 2
3 nfv 1707 . 2
4 nfvd 1708 . 2
51, 2, 3, 4sbciedf 3363 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator