Theorem vtoclg 2786

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)

Hypotheses

Ref	Expression
vtoclg.1	|- ( x = A -> ( ph <-> ps ) )
vtoclg.2	|- ph

Assertion

Ref	Expression
vtoclg	|- ( A e. V -> ps )

Distinct variable groups:   x, A   ps, x

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		nfcv 2308	. 2 |- F/_ x A
2		nfv 1516	. 2 |- F/ x ps
3		vtoclg.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4		vtoclg.2	. 2 |- ph
5	1, 2, 3, 4	vtoclgf 2784	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728

This theorem is referenced by:  vtoclbg  2787  ceqex  2853  mo2icl  2905  nelrdva  2933  sbctt  3017  sbcnestgf  3096  csbing  3329  ifmdc  3558  prnzg  3700  sneqrg  3742  unisng  3806  csbopabg  4060  trss  4089  inex1g  4118  ssexg  4121  pwexg  4159  prexg  4189  opth  4215  ordelord  4359  uniexg  4417  vtoclr  4652  resieq  4894  csbima12g  4965  dmsnsnsng  5081  iota5  5173  csbiotag  5181  funmo  5203  fconstg  5384  funfveu  5499  funbrfv  5525  fnbrfvb  5527  fvelimab  5542  ssimaexg  5548  fvelrn  5616  isoselem  5788  csbriotag  5810  csbov123g  5880  ovg  5980  tfrexlem  6302  rdg0g  6356  ensn1g  6763  fundmeng  6773  xpdom2g  6798  phplem3g  6822  prcdnql  7425  prcunqu  7426  prdisj  7433  shftvalg  10778  shftval4g  10779  climshft  11245  telfsumo  11407  fsumparts  11411  lcmgcdlem  12009  fiinopn  12642  bdzfauscl  13772  bdinex1g  13783  bdssexg  13786  bj-prexg  13793  bj-uniexg  13800