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

Theorem sbcied 3350
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)
Hypotheses
Ref Expression
sbcied.1  |-  ( ph  ->  A  e.  V )
sbcied.2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
sbcied  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Distinct variable groups:    x, A    ph, x    ch, x
Allowed substitution hints:    ps( x)    V( x)

Proof of Theorem sbcied
StepHypRef Expression
1 sbcied.1 . 2  |-  ( ph  ->  A  e.  V )
2 sbcied.2 . 2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
3 nfv 1694 . 2  |-  F/ x ph
4 nfvd 1695 . 2  |-  ( ph  ->  F/ x ch )
51, 2, 3, 4sbciedf 3349 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    e. wcel 1804   [.wsbc 3313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-sbc 3314
This theorem is referenced by:  sbcied2  3351  sbc2iedv  3390  sbc3ie  3391  sbcralt  3394  euotd  4738  fmptsnd  6078  riota5f  6267  fpwwe2lem12  9022  fpwwe2lem13  9023  sbcie3s  14553  issubc  15081  gsumvalx  15771  dmdprd  16903  dprdval  16908  dprdvalOLD  16910  issrg  17033  issrng  17373  islmhm  17547  isassa  17838  isphl  18536  istmd  20446  istgp  20449  isnlm  21057  isclm  21437  iscph  21490  iscms  21657  limcfval  22149  sbcies  27253  abfmpeld  27364  abfmpel  27365  isomnd  27564  isorng  27662
  Copyright terms: Public domain W3C validator