Theorem vtoclg 2658

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

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603

This theorem is referenced by:  vtoclbg  2659  ceqex  2722  mo2icl  2771  nelrdva  2797  sbctt  2880  sbcnestgf  2953  csbing  3173  prnzg  3514  sneqrg  3554  unisng  3618  csbopabg  3856  trss  3884  inex1g  3914  ssexg  3917  pwexg  3954  prexg  3966  opth  3992  ordelord  4136  uniexg  4193  vtoclr  4406  resieq  4640  csbima12g  4706  dmsnsnsng  4818  iota5  4907  csbiotag  4915  funmo  4937  fconstg  5103  funfveu  5208  funbrfv  5233  fnbrfvb  5235  fvelimab  5250  ssimaexg  5256  fvelrn  5319  isoselem  5479  csbriotag  5500  csbov123g  5563  ovg  5659  tfrexlem  5971  rdg0g  5998  ensn1g  6300  fundmeng  6310  xpdom2g  6329  phplem3g  6342  prcdnql  6674  prcunqu  6675  prdisj  6682  shftvalg  9724  shftval4g  9725  climshft  10143  lcmgcdlem  10459  bdzfauscl  10681  bdinex1g  10692  bdssexg  10695  bj-prexg  10702  bj-uniexg  10709