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

Theorem sbcie 3219
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 3217 . 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 184    = wceq 1369    e. wcel 1756   _Vcvv 2970   [.wsbc 3184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-v 2972  df-sbc 3185
This theorem is referenced by:  tfinds2  6472  findcard2  7550  ac6sfi  7554  ac6num  8646  fpwwe  8811  nn1suc  10341  wrdind  12369  cjth  12590  prmind2  13772  joinlem  15179  meetlem  15193  mrcmndind  15492  isghm  15745  issrg  16607  islmod  16950  islindf  18239  fgcl  19449  cfinfil  19464  csdfil  19465  supfil  19466  fin1aufil  19503  quotval  21756  fprodser  27460  soseq  27713  sdclem2  28635  fdc  28638  fdc1  28639  rabren3dioph  29151  2nn0ind  29283  zindbi  29284  onfrALTlem5  31247  bnj62  31706  bnj610  31736  bnj976  31768  bnj106  31858  bnj125  31862  bnj154  31868  bnj155  31869  bnj526  31878  bnj540  31882  bnj591  31901  bnj609  31907  bnj893  31918  bnj1417  32029  lshpkrlem3  32754  hdmap1fval  35439  hdmapfval  35472
  Copyright terms: Public domain W3C validator