Theorem vtoclg 2812

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 2332	. 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 2810	1 |- ( A e. V -> ps )

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

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 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754

This theorem is referenced by:  vtoclbg  2813  ceqex  2879  mo2icl  2931  nelrdva  2959  sbctt  3044  sbcnestgf  3123  csbing  3357  ifmdc  3589  prnzg  3731  sneqrg  3777  unisng  3841  csbopabg  4096  trss  4125  inex1g  4154  ssexg  4157  pwexg  4198  prexg  4229  opth  4255  ordelord  4399  uniexg  4457  vtoclr  4692  resieq  4935  csbima12g  5007  dmsnsnsng  5124  iotaexab  5214  iota5  5217  csbiotag  5228  funmo  5250  fconstg  5431  funfveu  5547  funbrfv  5575  fnbrfvb  5577  fvelimab  5593  ssimaexg  5599  fvelrn  5668  isoselem  5842  csbriotag  5865  csbov123g  5935  ovg  6036  tfrexlem  6360  rdg0g  6414  ensn1g  6824  fundmeng  6834  xpdom2g  6859  phplem3g  6885  prcdnql  7514  prcunqu  7515  prdisj  7522  shftvalg  10880  shftval4g  10881  climshft  11347  telfsumo  11509  fsumparts  11513  lcmgcdlem  12112  fiinopn  13981  bdzfauscl  15120  bdinex1g  15131  bdssexg  15134  bj-prexg  15141  bj-uniexg  15148