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

Theorem sbcied 3199
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 1630 . 2  |-  F/ x ph
4 nfvd 1631 . 2  |-  ( ph  ->  F/ x ch )
51, 2, 3, 4sbciedf 3198 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   [.wsbc 3163
This theorem is referenced by:  sbcied2  3200  sbc2iedv  3231  sbc3ie  3232  sbcralt  3235  euotd  4459  riota5f  6576  fpwwe2lem12  8518  fpwwe2lem13  8519  issubc  14037  gsumvalx  14776  dmdprd  15561  dprdval  15563  issrng  15940  islmhm  16105  isassa  16377  isphl  16861  istmd  18106  istgp  18109  isnlm  18713  isclm  19091  iscph  19135  iscms  19300  limcfval  19761  abfmpeld  24068  abfmpel  24069  isofld  24237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164
  Copyright terms: Public domain W3C validator