Theorem vtoclga 2804

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 2803	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 2740

This theorem is referenced by:  vtoclri  2813  ssuni  3832  ordtriexmid  4521  onsucsssucexmid  4527  tfis3  4586  fvmpt3  5596  fvmptssdm  5601  fnressn  5703  fressnfv  5704  caovord  6046  caovimo  6068  tfrlem1  6309  nnacl  6481  nnmcl  6482  nnacom  6485  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  nnsucsssuc  6493  nntri3or  6494  nnaordi  6509  nnaword  6512  nnmordi  6517  nnaordex  6529  ixpfn  6704  findcard  6888  findcard2  6889  findcard2s  6890  exmidomni  7140  indpi  7341  prarloclem3  7496  uzind4s2  9591  cnref1o  9650  frec2uzrdg  10409  expcl2lemap  10532  seq3coll  10822  climub  11352  climserle  11353  fsum3cvg  11386  summodclem2a  11389  prodfap0  11553  prodfrecap  11554  fproddccvg  11580  alginv  12047  algcvg  12048  algcvga  12051  algfx  12052  prmind2  12120  prmpwdvds  12353  lgsdir2lem4  14435