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

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

Proof of Theorem sbcied2
StepHypRef Expression
1 sbcied2.1 . 2  |-  ( ph  ->  A  e.  V )
2 id 22 . . . 4  |-  ( x  =  A  ->  x  =  A )
3 sbcied2.2 . . . 4  |-  ( ph  ->  A  =  B )
42, 3sylan9eqr 2445 . . 3  |-  ( (
ph  /\  x  =  A )  ->  x  =  B )
5 sbcied2.3 . . 3  |-  ( (
ph  /\  x  =  B )  ->  ( ps 
<->  ch ) )
64, 5syldan 468 . 2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
71, 6sbcied 3289 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826   [.wsbc 3252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-v 3036  df-sbc 3253
This theorem is referenced by:  iscat  15079  sectffval  15156  issubc  15241  isfunc  15270  ismgm  15990  issgrp  16029  ismndOLD  16043  isnsg  16347  isring  17315  islbs  17835  isdomn  18056  isassa  18077  opsrval  18252  isuhgr  32684  isushgr  32685  isrng  32882
  Copyright terms: Public domain W3C validator