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

Theorem sbcied 3040
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 1609 . 2  |-  F/ x ph
4 nfvd 1610 . 2  |-  ( ph  ->  F/ x ch )
51, 2, 3, 4sbciedf 3039 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   [.wsbc 3004
This theorem is referenced by:  sbcied2  3041  sbc2iedv  3072  sbc3ie  3073  sbcralt  3076  euotd  4283  riota5f  6345  fpwwe2lem12  8279  fpwwe2lem13  8280  issubc  13728  gsumvalx  14467  dmdprd  15252  dprdval  15254  issrng  15631  islmhm  15800  isassa  16072  isphl  16548  istmd  17773  istgp  17776  isnlm  18202  isclm  18578  iscph  18622  iscms  18783  limcfval  19238  abfmpeld  23233  abfmpel  23234
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005
  Copyright terms: Public domain W3C validator