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

Theorem vtocl 3147
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
Hypotheses
Ref Expression
vtocl.1  |-  A  e. 
_V
vtocl.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtocl.3  |-  ph
Assertion
Ref Expression
vtocl  |-  ps
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem vtocl
StepHypRef Expression
1 nfv 1694 . 2  |-  F/ x ps
2 vtocl.1 . 2  |-  A  e. 
_V
3 vtocl.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtocl.3 . 2  |-  ph
51, 2, 3, 4vtoclf 3146 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804   _Vcvv 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097
This theorem is referenced by:  vtoclb  3150  zfauscl  4560  pwex  4620  fnbrfvb  5898  caovcan  6464  uniex  6581  findcard2  7762  zfregcl  8023  bnd2  8314  kmlem2  8534  axcc2lem  8819  dominf  8828  dcomex  8830  ac4c  8859  ac5  8860  dominfac  8951  pwfseqlem4  9043  grothomex  9210  ramub2  14409  ismred2  14877  dvfsumlem2  22301  plydivlem4  22564  frmin  29297  voliunnfl  30033  volsupnfl  30034  prdsbnd2  30266  iscringd  30371  monotoddzzfi  30853  monotoddzz  30854  dvgrat  31169  cvgdvgrat  31170  fourierdlem41  31819  fourierdlem48  31826  fourierdlem49  31827  fourierdlem51  31829  fourierdlem71  31849  fourierdlem83  31861  fourierdlem97  31875  bnj865  33709  bnj1015  33747
  Copyright terms: Public domain W3C validator