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  5725  fvmptssdm  5731  fnressn  5840  fressnfv  5841  caovord  6194  caovimo  6216  tfrlem1  6474  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnsucsssuc  6660  nntri3or  6661  nnaordi  6676  nnaword  6679  nnmordi  6684  nnaordex  6696  ixpfn  6873  findcard  7077  findcard2  7078  findcard2s  7079  exmidomni  7341  indpi  7562  prarloclem3  7717  uzind4s2  9825  cnref1o  9885  frec2uzrdg  10671  expcl2lemap  10813  seq3coll  11106  climub  11905  climserle  11906  fsum3cvg  11940  summodclem2a  11943  prodfap0  12107  prodfrecap  12108  fproddccvg  12134  alginv  12620  algcvg  12621  algcvga  12624  algfx  12625  prmind2  12693  prmpwdvds  12929  lgsdir2lem4  15762