Theorem vtoclg 2672

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

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1287   e. wcel 1436

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 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617

This theorem is referenced by:  vtoclbg  2673  ceqex  2735  mo2icl  2785  nelrdva  2811  sbctt  2894  sbcnestgf  2968  csbing  3196  ifmdc  3414  prnzg  3549  sneqrg  3591  unisng  3655  csbopabg  3893  trss  3922  inex1g  3952  ssexg  3955  pwexg  3992  prexg  4014  opth  4040  ordelord  4184  uniexg  4241  vtoclr  4456  resieq  4693  csbima12g  4762  dmsnsnsng  4876  iota5  4968  csbiotag  4976  funmo  4998  fconstg  5172  funfveu  5283  funbrfv  5308  fnbrfvb  5310  fvelimab  5325  ssimaexg  5331  fvelrn  5395  isoselem  5562  csbriotag  5583  csbov123g  5646  ovg  5742  tfrexlem  6055  rdg0g  6109  ensn1g  6468  fundmeng  6478  xpdom2g  6502  phplem3g  6526  prcdnql  6990  prcunqu  6991  prdisj  6998  shftvalg  10170  shftval4g  10171  climshft  10590  lcmgcdlem  10965  bdzfauscl  11250  bdinex1g  11261  bdssexg  11264  bj-prexg  11271  bj-uniexg  11278