Theorem vtoclga 2805

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 2319	. 2 |- F/_ x A
2		nfv 1528	. 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 2804	1 |- ( A e. B -> 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:  vtoclri  2814  ssuni  3833  ordtriexmid  4522  onsucsssucexmid  4528  tfis3  4587  fvmpt3  5598  fvmptssdm  5603  fnressn  5705  fressnfv  5706  caovord  6049  caovimo  6071  tfrlem1  6312  nnacl  6484  nnmcl  6485  nnacom  6488  nnaass  6489  nndi  6490  nnmass  6491  nnmsucr  6492  nnmcom  6493  nnsucsssuc  6496  nntri3or  6497  nnaordi  6512  nnaword  6515  nnmordi  6520  nnaordex  6532  ixpfn  6707  findcard  6891  findcard2  6892  findcard2s  6893  exmidomni  7143  indpi  7344  prarloclem3  7499  uzind4s2  9594  cnref1o  9653  frec2uzrdg  10412  expcl2lemap  10535  seq3coll  10825  climub  11355  climserle  11356  fsum3cvg  11389  summodclem2a  11392  prodfap0  11556  prodfrecap  11557  fproddccvg  11583  alginv  12050  algcvg  12051  algcvga  12054  algfx  12055  prmind2  12123  prmpwdvds  12356  lgsdir2lem4  14593