Theorem vtoclga 2880

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 2384	. 2 |- F/_ x A
2		nfv 1577	. 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 2879	1 |- ( A e. B -> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2203

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814

This theorem is referenced by:  vtoclri  2891  ssuni  3935  ordtriexmid  4642  onsucsssucexmid  4648  tfis3  4707  fvmpt3  5755  fvmptssdm  5761  fnressn  5869  fressnfv  5870  caovord  6225  caovimo  6247  tfrlem1  6538  nnacl  6712  nnmcl  6713  nnacom  6716  nnaass  6717  nndi  6718  nnmass  6719  nnmsucr  6720  nnmcom  6721  nnsucsssuc  6724  nntri3or  6725  nnaordi  6740  nnaword  6743  nnmordi  6748  nnaordex  6760  ixpfn  6938  findcard  7144  findcard2  7145  findcard2s  7146  exmidomni  7432  indpi  7656  prarloclem3  7811  uzind4s2  9922  cnref1o  9982  frec2uzrdg  10770  expcl2lemap  10912  seq3coll  11210  climub  12025  climserle  12026  fsum3cvg  12060  summodclem2a  12063  prodfap0  12227  prodfrecap  12228  fproddccvg  12254  alginv  12740  algcvg  12741  algcvga  12744  algfx  12745  prmind2  12813  prmpwdvds  13049  lgsdir2lem4  15896