Theorem vtocl 2877

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 1581	. 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 2876	1 |- ps

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   _Vcvv 2821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  vtoclb  2880  zfausclOLD  4248  bnd2  4305  uniex  4578  ordtriexmid  4663  onsucsssucexmid  4669  regexmid  4677  ordsoexmid  4704  onintexmid  4715  reg3exmid  4722  nnregexmid  4763  acexmidlemv  6073  caovcan  6244  findcard2  7183  findcard2s  7184  inffiexmid  7203  sup3exmid  9277  bj-uniex  16857  bj-omtrans  16896