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

Theorem sbcie 3314
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)
Hypotheses
Ref Expression
sbcie.1  |-  A  e. 
_V
sbcie.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
sbcie  |-  ( [. A  /  x ]. ph  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem sbcie
StepHypRef Expression
1 sbcie.1 . 2  |-  A  e. 
_V
2 sbcie.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3312 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3ax-mp 5 1  |-  ( [. A  /  x ]. ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455    e. wcel 1898   _Vcvv 3057   [.wsbc 3279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059  df-sbc 3280
This theorem is referenced by:  tfinds2  6717  findcard2  7837  ac6sfi  7841  ac6num  8935  fpwwe  9097  nn1suc  10658  wrdind  12870  cjth  13215  fprodser  14052  prmind2  14684  joinlem  16306  meetlem  16320  mrcmndind  16662  isghm  16932  islmod  18144  islindf  19419  fgcl  20942  cfinfil  20957  csdfil  20958  supfil  20959  fin1aufil  20996  quotval  23294  bnj62  29575  bnj610  29606  bnj976  29638  bnj106  29728  bnj125  29732  bnj154  29738  bnj155  29739  bnj526  29748  bnj540  29752  bnj591  29771  bnj609  29777  bnj893  29788  bnj1417  29899  soseq  30541  poimirlem27  32012  sdclem2  32116  fdc  32119  fdc1  32120  lshpkrlem3  32723  hdmap1fval  35410  hdmapfval  35443  rabren3dioph  35703  2nn0ind  35838  zindbi  35839  onfrALTlem5  36952  dfconngr1  39929  isconngr  39930  isconngr1  39931
  Copyright terms: Public domain W3C validator