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

Step	Hyp	Ref	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
5	1, 2, 3, 4	vtoclf 3146	1 |- ps

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