Theorem vtoclg 2790

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   e. wcel 2141

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732

This theorem is referenced by:  vtoclbg  2791  ceqex  2857  mo2icl  2909  nelrdva  2937  sbctt  3021  sbcnestgf  3100  csbing  3334  ifmdc  3565  prnzg  3707  sneqrg  3749  unisng  3813  csbopabg  4067  trss  4096  inex1g  4125  ssexg  4128  pwexg  4166  prexg  4196  opth  4222  ordelord  4366  uniexg  4424  vtoclr  4659  resieq  4901  csbima12g  4972  dmsnsnsng  5088  iota5  5180  csbiotag  5191  funmo  5213  fconstg  5394  funfveu  5509  funbrfv  5535  fnbrfvb  5537  fvelimab  5552  ssimaexg  5558  fvelrn  5627  isoselem  5799  csbriotag  5821  csbov123g  5891  ovg  5991  tfrexlem  6313  rdg0g  6367  ensn1g  6775  fundmeng  6785  xpdom2g  6810  phplem3g  6834  prcdnql  7446  prcunqu  7447  prdisj  7454  shftvalg  10800  shftval4g  10801  climshft  11267  telfsumo  11429  fsumparts  11433  lcmgcdlem  12031  fiinopn  12796  bdzfauscl  13925  bdinex1g  13936  bdssexg  13939  bj-prexg  13946  bj-uniexg  13953