Theorem vtoclg 2821

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762

This theorem is referenced by:  vtoclbg  2822  ceqex  2888  mo2icl  2940  nelrdva  2968  sbctt  3053  sbcnestgf  3133  csbing  3367  ifmdc  3598  prnzg  3743  sneqrg  3789  unisng  3853  csbopabg  4108  trss  4137  inex1g  4166  ssexg  4169  pwexg  4210  prexg  4241  opth  4267  ordelord  4413  uniexg  4471  vtoclr  4708  resieq  4953  csbima12g  5027  dmsnsnsng  5144  iotaexab  5234  iota5  5237  csbiotag  5248  funmo  5270  fconstg  5451  funfveu  5568  funbrfv  5596  fnbrfvb  5598  fvelimab  5614  ssimaexg  5620  fvelrn  5690  isoselem  5864  csbriotag  5887  csbov123g  5957  ovg  6059  tfrexlem  6389  rdg0g  6443  ensn1g  6853  fundmeng  6863  xpdom2g  6888  phplem3g  6914  prcdnql  7546  prcunqu  7547  prdisj  7554  shftvalg  10983  shftval4g  10984  climshft  11450  telfsumo  11612  fsumparts  11616  lcmgcdlem  12218  fiinopn  14183  bdzfauscl  15452  bdinex1g  15463  bdssexg  15466  bj-prexg  15473  bj-uniexg  15480