Theorem vtoclg 2799

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2148

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741

This theorem is referenced by:  vtoclbg  2800  ceqex  2866  mo2icl  2918  nelrdva  2946  sbctt  3031  sbcnestgf  3110  csbing  3344  ifmdc  3576  prnzg  3718  sneqrg  3764  unisng  3828  csbopabg  4083  trss  4112  inex1g  4141  ssexg  4144  pwexg  4182  prexg  4213  opth  4239  ordelord  4383  uniexg  4441  vtoclr  4676  resieq  4919  csbima12g  4991  dmsnsnsng  5108  iota5  5200  csbiotag  5211  funmo  5233  fconstg  5414  funfveu  5530  funbrfv  5556  fnbrfvb  5558  fvelimab  5574  ssimaexg  5580  fvelrn  5649  isoselem  5823  csbriotag  5845  csbov123g  5915  ovg  6015  tfrexlem  6337  rdg0g  6391  ensn1g  6799  fundmeng  6809  xpdom2g  6834  phplem3g  6858  prcdnql  7485  prcunqu  7486  prdisj  7493  shftvalg  10847  shftval4g  10848  climshft  11314  telfsumo  11476  fsumparts  11480  lcmgcdlem  12079  fiinopn  13543  bdzfauscl  14681  bdinex1g  14692  bdssexg  14695  bj-prexg  14702  bj-uniexg  14709