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

Theorem sbcied 3324
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 1674 . 2  |-  F/ x ph
4 nfvd 1675 . 2  |-  ( ph  ->  F/ x ch )
51, 2, 3, 4sbciedf 3323 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    e. wcel 1758   [.wsbc 3287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3073  df-sbc 3288
This theorem is referenced by:  sbcied2  3325  sbc2iedv  3364  sbc3ie  3365  sbcralt  3368  euotd  4693  riota5f  6179  fpwwe2lem12  8912  fpwwe2lem13  8913  sbcie3s  14329  issubc  14859  gsumvalx  15613  dmdprd  16594  dprdval  16599  dprdvalOLD  16601  issrg  16723  issrng  17050  islmhm  17223  isassa  17502  isphl  18175  istmd  19770  istgp  19773  isnlm  20381  isclm  20761  iscph  20814  iscms  20981  limcfval  21473  sbcies  26011  abfmpeld  26113  abfmpel  26114  isomnd  26302  isorng  26405  fmptsnd  30863
  Copyright terms: Public domain W3C validator