Theorem vtoclga 3272

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 2764	. 2 |- F/_ x A
2		nfv 1843	. 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 3271	1 |- ( A e. B -> ps )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202

This theorem is referenced by:  vtoclri  3283  ssuniOLD  4460  disjxiun  4649  disjxiunOLD  4650  wfis3  5721  opabiota  6261  fvmpt3  6286  fvmptss  6292  fnressn  6425  fressnfv  6427  caovord  6845  caovmo  6871  ordunisuc  7032  tfis3  7057  wfr2a  7432  onfununi  7438  smogt  7464  tz7.44-1  7502  tz7.44-2  7503  tz7.44-3  7504  nnacl  7691  nnmcl  7692  nnecl  7693  nnacom  7697  nnaass  7702  nndi  7703  nnmass  7704  nnmsucr  7705  nnmcom  7706  nnmordi  7711  ixpfn  7914  findcard  8199  findcard2  8200  marypha1  8340  cantnfle  8568  cantnflem1  8586  cnfcom  8597  fseqenlem1  8847  ackbij1lem5  9046  ackbij1lem8  9049  cardcf  9074  cfsmolem  9092  wunex2  9560  ingru  9637  recrecnq  9789  prlem934  9855  nn1suc  11041  uzind4s2  11749  rpnnen1lem6  11819  rpnnen1OLD  11825  cnref1o  11827  xmulasslem  12115  om2uzsuci  12747  expcl2lem  12872  hashmap  13222  hashpw  13223  seqcoll  13248  climub  14392  climserle  14393  sumrblem  14442  fsumcvg  14443  summolem2a  14446  infcvgaux2i  14590  prodfn0  14626  prodfrec  14627  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  divalglem8  15123  bezoutlem1  15256  alginv  15288  algcvg  15289  algcvga  15292  algfx  15293  prmind2  15398  prmpwdvds  15608  cnextfvval  21869  xrsxmet  22612  xrhmeo  22745  cmetcaulem  23086  bcth3  23128  itg2addlem  23525  taylfval  24113  sinord  24280  logexprlim  24950  lgsdir2lem4  25053  hlim2  28049  elnlfn  28787  lnconi  28892  chirredlem3  29251  chirredlem4  29252  cnre2csqlem  29956  eulerpartlemsf  30421  eulerpartlemn  30443  bnj1321  31095  bnj1418  31108  subfacp1lem1  31161  frins3  31748  nn0prpwlem  32317  findreccl  32452  mptsnunlem  33185  rdgeqoa  33218  poimirlem22  33431  poimirlem26  33435  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  ftc1anclem3  33487  ftc1anclem8  33492  sdclem2  33538  iscringd  33797  renegclALT  34249  zindbi  37511  fmuldfeq  39815  sumnnodd  39862  iblspltprt  40189  stoweidlem2  40219  stoweidlem17  40234  stoweidlem21  40238  stoweidlem43  40260  stoweidlem51  40268  wallispi  40287