Theorem vtoclg 2795

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2146

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737

This theorem is referenced by:  vtoclbg  2796  ceqex  2862  mo2icl  2914  nelrdva  2942  sbctt  3027  sbcnestgf  3106  csbing  3340  ifmdc  3571  prnzg  3713  sneqrg  3758  unisng  3822  csbopabg  4076  trss  4105  inex1g  4134  ssexg  4137  pwexg  4175  prexg  4205  opth  4231  ordelord  4375  uniexg  4433  vtoclr  4668  resieq  4910  csbima12g  4982  dmsnsnsng  5098  iota5  5190  csbiotag  5201  funmo  5223  fconstg  5404  funfveu  5520  funbrfv  5546  fnbrfvb  5548  fvelimab  5564  ssimaexg  5570  fvelrn  5639  isoselem  5811  csbriotag  5833  csbov123g  5903  ovg  6003  tfrexlem  6325  rdg0g  6379  ensn1g  6787  fundmeng  6797  xpdom2g  6822  phplem3g  6846  prcdnql  7458  prcunqu  7459  prdisj  7466  shftvalg  10813  shftval4g  10814  climshft  11280  telfsumo  11442  fsumparts  11446  lcmgcdlem  12044  fiinopn  13082  bdzfauscl  14211  bdinex1g  14222  bdssexg  14225  bj-prexg  14232  bj-uniexg  14239