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

Theorem sbcied 3361
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 1712 . 2  |-  F/ x ph
4 nfvd 1713 . 2  |-  ( ph  ->  F/ x ch )
51, 2, 3, 4sbciedf 3360 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108  df-sbc 3325
This theorem is referenced by:  sbcied2  3362  sbc2iedv  3393  sbc3ie  3394  sbcralt  3397  euotd  4737  fmptsnd  6069  riota5f  6256  fpwwe2lem12  9008  fpwwe2lem13  9009  sbcie3s  14762  issubc  15323  gsumvalx  16096  dmdprd  17224  dprdval  17229  dprdvalOLD  17231  issrg  17354  issrng  17694  islmhm  17868  isassa  18159  isphl  18836  istmd  20739  istgp  20742  isnlm  21350  isclm  21730  iscph  21783  iscms  21950  limcfval  22442  sbcies  27579  abfmpeld  27713  abfmpel  27714  isomnd  27925  isorng  28024
  Copyright terms: Public domain W3C validator