Theorem vtoclg 2781

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1342   e. wcel 2135

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723

This theorem is referenced by:  vtoclbg  2782  ceqex  2848  mo2icl  2900  nelrdva  2928  sbctt  3012  sbcnestgf  3091  csbing  3324  ifmdc  3552  prnzg  3694  sneqrg  3736  unisng  3800  csbopabg  4054  trss  4083  inex1g  4112  ssexg  4115  pwexg  4153  prexg  4183  opth  4209  ordelord  4353  uniexg  4411  vtoclr  4646  resieq  4888  csbima12g  4959  dmsnsnsng  5075  iota5  5167  csbiotag  5175  funmo  5197  fconstg  5378  funfveu  5493  funbrfv  5519  fnbrfvb  5521  fvelimab  5536  ssimaexg  5542  fvelrn  5610  isoselem  5782  csbriotag  5804  csbov123g  5871  ovg  5971  tfrexlem  6293  rdg0g  6347  ensn1g  6754  fundmeng  6764  xpdom2g  6789  phplem3g  6813  prcdnql  7416  prcunqu  7417  prdisj  7424  shftvalg  10764  shftval4g  10765  climshft  11231  telfsumo  11393  fsumparts  11397  lcmgcdlem  11988  fiinopn  12543  bdzfauscl  13607  bdinex1g  13618  bdssexg  13621  bj-prexg  13628  bj-uniexg  13635