Theorem vtocl 2857

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 1576	. 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 2856	1 |- ps

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   e. wcel 2201   _Vcvv 2801

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-v 2803

This theorem is referenced by:  vtoclb  2860  zfauscl  4210  bnd2  4265  uniex  4536  ordtriexmid  4621  onsucsssucexmid  4627  regexmid  4635  ordsoexmid  4662  onintexmid  4673  reg3exmid  4680  nnregexmid  4721  acexmidlemv  6021  caovcan  6192  findcard2  7083  findcard2s  7084  inffiexmid  7103  sup3exmid  9142  bj-uniex  16572  bj-omtrans  16611