Theorem vtoclga 2827

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 2336	. 2 |- F/_ x A
2		nfv 1539	. 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 2826	1 |- ( A e. B -> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2164

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762

This theorem is referenced by:  vtoclri  2836  ssuni  3858  ordtriexmid  4554  onsucsssucexmid  4560  tfis3  4619  fvmpt3  5637  fvmptssdm  5643  fnressn  5745  fressnfv  5746  caovord  6092  caovimo  6114  tfrlem1  6363  nnacl  6535  nnmcl  6536  nnacom  6539  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  nnsucsssuc  6547  nntri3or  6548  nnaordi  6563  nnaword  6566  nnmordi  6571  nnaordex  6583  ixpfn  6760  findcard  6946  findcard2  6947  findcard2s  6948  exmidomni  7203  indpi  7404  prarloclem3  7559  uzind4s2  9659  cnref1o  9719  frec2uzrdg  10483  expcl2lemap  10625  seq3coll  10916  climub  11490  climserle  11491  fsum3cvg  11524  summodclem2a  11527  prodfap0  11691  prodfrecap  11692  fproddccvg  11718  alginv  12188  algcvg  12189  algcvga  12192  algfx  12193  prmind2  12261  prmpwdvds  12496  lgsdir2lem4  15188