Theorem vtoclg 2914

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 2489	. 2 |- F/_xA
2		nfv 1619	. 2 |- F/xps
3		vtoclg.1	. 2 |- (x = A -> (ph <-> ps))
4		vtoclg.2	. 2 |- ph
5	1, 2, 3, 4	vtoclgf 2913	1 |- (A e. V -> ps)

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861

This theorem is referenced by:  vtoclbg  2915  ceqex  2969  moeq3  3013  mo2icl  3015  sbctt  3108  sbcnestgf  3183  csbing  3462  csbifg  3690  prnzg  3836  sneqrg  3874  unisng  3908  snex  4111  snel1cg  4141  xpkvexg  4285  cnvkexg  4286  p6exg  4290  sikexg  4296  ins2kexg  4305  ins3kexg  4306  iota5  4359  csbiotag  4371  ssfin  4470  csbopabg  4637  vtoclr  4816  csbima12g  4955  dmsnopg  5066  fconstg  5251  fvelimab  5370  fvi  5442  csbovg  5552  trtxp  5781  oqelins4  5794  fnfullfunlem1  5856  fvfullfun  5864  fundmeng  6044  df1c3g  6141  sbthlem2  6204  frecxp  6314  frecxpg  6315