MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclga Unicode version

Theorem vtoclga 2977
Description: Implicit substitution of a class for a set 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
StepHypRef Expression
1 nfcv 2540 . 2  |-  F/_ x A
2 nfv 1626 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 2976 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721
This theorem is referenced by:  vtoclri  2986  ssuni  3997  disjxiun  4169  ordunisuc  4771  tfis3  4796  fvmpt3  5767  fvmptss  5772  fnressn  5877  fressnfv  5879  caovord  6217  caovmo  6243  opabiota  6497  onfununi  6562  smogt  6588  tfrlem1  6595  tz7.44-1  6623  tz7.44-2  6624  tz7.44-3  6625  nnacl  6813  nnmcl  6814  nnecl  6815  nnacom  6819  nnaass  6824  nndi  6825  nnmass  6826  nnmsucr  6827  nnmcom  6828  nnmordi  6833  ixpfn  7027  findcard  7306  findcard2  7307  marypha1  7397  cantnfle  7582  cantnflem1  7601  cnfcom  7613  fseqenlem1  7861  ackbij1lem5  8060  ackbij1lem8  8063  cardcf  8088  cfsmolem  8106  wunex2  8569  ingru  8646  recrecnq  8800  prlem934  8866  nn1suc  9977  uzind4s2  10493  rpnnen1  10561  cnref1o  10563  xmulasslem  10820  om2uzsuci  11243  expcl2lem  11348  hashmap  11653  hashpw  11654  seqcoll  11667  climub  12410  climserle  12411  sumrblem  12460  fsumcvg  12461  summolem2a  12464  infcvgaux2i  12592  divalglem8  12875  bezoutlem1  12993  alginv  13021  algcvg  13022  algcvga  13025  algfx  13026  isprm2lem  13041  prmind2  13045  prmpwdvds  13227  cnextfvval  18049  xrsxmet  18793  xrhmeo  18924  cmetcaulem  19194  bcth3  19237  itg2addlem  19603  taylfval  20228  sinord  20389  logexprlim  20962  lgsdir2lem4  21063  hlim2  22647  elnlfn  23384  lnconi  23489  chirredlem3  23848  chirredlem4  23849  cnre2csqlem  24261  subfacp1lem1  24818  prodfn0  25175  prodfrec  25176  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  wfis3  25429  frins3  25465  wfr2  25487  wfr2c  25488  findreccl  26107  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  nn0prpwlem  26215  sdclem2  26336  iscringd  26499  zindbi  26899  fmuldfeq  27580  stoweidlem2  27618  stoweidlem17  27633  stoweidlem21  27637  stoweidlem34  27650  stoweidlem42  27658  stoweidlem43  27659  stoweidlem48  27664  stoweidlem51  27667  wallispi  27686  bnj1321  29102  bnj1418  29115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918
  Copyright terms: Public domain W3C validator