Theorem vtocle 3187

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.)

Hypotheses

Ref	Expression
vtocle.1	|- A e. _V
vtocle.2	|- ( x = A -> ph )

Assertion

Ref	Expression
vtocle	|- ph

Distinct variable groups:   x, A   ph, x

Proof of Theorem vtocle

Step	Hyp	Ref	Expression
1		vtocle.1	. 2 |- A e. _V
2		vtocle.2	. . 3 |- ( x = A -> ph )
3	2	vtocleg 3184	. 2 |- ( A e. _V -> ph )
4	1, 3	ax-mp 5	1 |- ph

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   _Vcvv 3113

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-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115

This theorem is referenced by:  zfrepclf  4564  tz6.12i  5884  eloprabga  6371  cfflb  8635  axcc3  8814  nn0ind-raph  10957