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

Theorem sbcieg 3369
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.)
Hypothesis
Ref Expression
sbcieg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
sbcieg  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Distinct variable groups:    x, A    ps, x
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem sbcieg
StepHypRef Expression
1 nfv 1683 . 2  |-  F/ x ps
2 sbcieg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2sbciegf 3368 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   [.wsbc 3336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3120  df-sbc 3337
This theorem is referenced by:  sbcie  3371  ralsng  4068  rexsng  4069  rabsnif  4102  ralrnmpt  6041  fpwwe2lem3  9023  nn1suc  10569  mrcmndind  15869  fgcl  20247  cfinfil  20262  csdfil  20263  supfil  20264  fin1aufil  20301  ifeqeqx  27242  nn0min  27435  2nn0ind  30809  zindbi  30810  trsbcVD  33158  onfrALTlem5VD  33166  bnj1452  33588  cdlemk35s  36134  cdlemk39s  36136  cdlemk42  36138
  Copyright terms: Public domain W3C validator