Theorem vtoclg 2824

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765

This theorem is referenced by:  vtoclbg  2825  ceqex  2891  mo2icl  2943  nelrdva  2971  sbctt  3056  sbcnestgf  3136  csbing  3371  ifmdc  3602  prnzg  3747  sneqrg  3793  unisng  3857  csbopabg  4112  trss  4141  inex1g  4170  ssexg  4173  pwexg  4214  prexg  4245  opth  4271  ordelord  4417  uniexg  4475  vtoclr  4712  resieq  4957  csbima12g  5031  dmsnsnsng  5148  iotaexab  5238  iota5  5241  csbiotag  5252  funmo  5274  fconstg  5457  funfveu  5574  funbrfv  5602  fnbrfvb  5604  fvelimab  5620  ssimaexg  5626  fvelrn  5696  isoselem  5870  csbriotag  5893  csbov123g  5964  ovg  6066  tfrexlem  6401  rdg0g  6455  ensn1g  6865  fundmeng  6875  xpdom2g  6900  phplem3g  6926  prcdnql  7568  prcunqu  7569  prdisj  7576  shftvalg  11018  shftval4g  11019  climshft  11486  telfsumo  11648  fsumparts  11652  lcmgcdlem  12270  fiinopn  14324  bdzfauscl  15620  bdinex1g  15631  bdssexg  15634  bj-prexg  15641  bj-uniexg  15648