Theorem vtoclga 2870

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)

Hypotheses

Ref	Expression
vtoclga.1	|- ( x = A -> ( ph <-> ps ) )
vtoclga.2	|- ( x e. B -> ph )

Assertion

Ref	Expression
vtoclga	|- ( A e. B -> ps )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem vtoclga

Step	Hyp	Ref	Expression
1		nfcv 2374	. 2 |- F/_ x A
2		nfv 1576	. 2 |- F/ x ps
3		vtoclga.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4		vtoclga.2	. 2 |- ( x e. B -> ph )
5	1, 2, 3, 4	vtoclgaf 2869	1 |- ( A e. B -> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   e. wcel 2202

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804

This theorem is referenced by:  vtoclri  2881  ssuni  3915  ordtriexmid  4619  onsucsssucexmid  4625  tfis3  4684  fvmpt3  5726  fvmptssdm  5732  fnressn  5841  fressnfv  5842  caovord  6197  caovimo  6219  tfrlem1  6477  nnacl  6651  nnmcl  6652  nnacom  6655  nnaass  6656  nndi  6657  nnmass  6658  nnmsucr  6659  nnmcom  6660  nnsucsssuc  6663  nntri3or  6664  nnaordi  6679  nnaword  6682  nnmordi  6687  nnaordex  6699  ixpfn  6876  findcard  7080  findcard2  7081  findcard2s  7082  exmidomni  7344  indpi  7565  prarloclem3  7720  uzind4s2  9828  cnref1o  9888  frec2uzrdg  10675  expcl2lemap  10817  seq3coll  11110  climub  11925  climserle  11926  fsum3cvg  11960  summodclem2a  11963  prodfap0  12127  prodfrecap  12128  fproddccvg  12154  alginv  12640  algcvg  12641  algcvga  12644  algfx  12645  prmind2  12713  prmpwdvds  12949  lgsdir2lem4  15787