Theorem vtoclg 2877

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 2386	. 2 |- F/_ x A
2		nfv 1577	. 2 |- F/ x ps
3		vtoclg.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4		vtoclg.2	. 2 |- ph
5	1, 2, 3, 4	vtoclgf 2875	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2205

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-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817

This theorem is referenced by:  vtoclbg  2878  ceqex  2947  mo2icl  2999  nelrdva  3027  sbctt  3112  sbcnestgf  3193  csbing  3432  ifmdc  3669  prnzg  3822  sneqrg  3871  unisng  3936  csbopabg  4193  trss  4222  inex1g  4251  ssexg  4254  pwexg  4298  prexg  4330  opth  4358  ordelord  4507  uniexg  4565  vtoclr  4803  resieq  5053  csbima12g  5128  dmsnsnsng  5245  iotaexab  5336  iota5  5339  csbiotag  5350  funmo  5372  fconstg  5569  funfveu  5688  funbrfv  5718  fnbrfvb  5720  fvelimab  5738  ssimaexg  5744  fvelrn  5813  isoselem  5999  csbriotag  6025  csbov123g  6097  ovg  6201  tfrexlem  6578  rdg0g  6632  ensn1g  7050  fundmeng  7061  xpdom2g  7096  phplem3g  7123  prcdnql  7815  prcunqu  7816  prdisj  7823  shftvalg  11546  shftval4g  11547  climshft  12014  telfsumo  12177  fsumparts  12181  lcmgcdlem  12799  fiinopn  14995  bdzfauscl  16786  bdinex1g  16797  bdssexg  16800  bj-prexg  16807  bj-uniexg  16814