Theorem vtoclg 2715

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1312   e. wcel 1461

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657

This theorem is referenced by:  vtoclbg  2716  ceqex  2780  mo2icl  2830  nelrdva  2858  sbctt  2941  sbcnestgf  3015  csbing  3247  ifmdc  3473  prnzg  3611  sneqrg  3653  unisng  3717  csbopabg  3964  trss  3993  inex1g  4022  ssexg  4025  pwexg  4062  prexg  4091  opth  4117  ordelord  4261  uniexg  4319  vtoclr  4545  resieq  4785  csbima12g  4856  dmsnsnsng  4972  iota5  5064  csbiotag  5072  funmo  5094  fconstg  5275  funfveu  5386  funbrfv  5412  fnbrfvb  5414  fvelimab  5429  ssimaexg  5435  fvelrn  5503  isoselem  5673  csbriotag  5694  csbov123g  5761  ovg  5861  tfrexlem  6182  rdg0g  6236  ensn1g  6642  fundmeng  6652  xpdom2g  6676  phplem3g  6700  prcdnql  7233  prcunqu  7234  prdisj  7241  shftvalg  10494  shftval4g  10495  climshft  10958  telfsumo  11120  fsumparts  11124  lcmgcdlem  11597  fiinopn  12007  bdzfauscl  12767  bdinex1g  12778  bdssexg  12781  bj-prexg  12788  bj-uniexg  12795