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

Theorem vtoclga 3019
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 2574 . 2  |-  F/_ x A
2 nfv 1630 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3018 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726
This theorem is referenced by:  vtoclri  3028  ssuni  4039  disjxiun  4211  ordunisuc  4814  tfis3  4839  fvmpt3  5810  fvmptss  5815  fnressn  5920  fressnfv  5922  caovord  6260  caovmo  6286  opabiota  6540  onfununi  6605  smogt  6631  tfrlem1  6638  tz7.44-1  6666  tz7.44-2  6667  tz7.44-3  6668  nnacl  6856  nnmcl  6857  nnecl  6858  nnacom  6862  nnaass  6867  nndi  6868  nnmass  6869  nnmsucr  6870  nnmcom  6871  nnmordi  6876  ixpfn  7070  findcard  7349  findcard2  7350  marypha1  7441  cantnfle  7628  cantnflem1  7647  cnfcom  7659  fseqenlem1  7907  ackbij1lem5  8106  ackbij1lem8  8109  cardcf  8134  cfsmolem  8152  wunex2  8615  ingru  8692  recrecnq  8846  prlem934  8912  nn1suc  10023  uzind4s2  10539  rpnnen1  10607  cnref1o  10609  xmulasslem  10866  om2uzsuci  11290  expcl2lem  11395  hashmap  11700  hashpw  11701  seqcoll  11714  climub  12457  climserle  12458  sumrblem  12507  fsumcvg  12508  summolem2a  12511  infcvgaux2i  12639  divalglem8  12922  bezoutlem1  13040  alginv  13068  algcvg  13069  algcvga  13072  algfx  13073  isprm2lem  13088  prmind2  13092  prmpwdvds  13274  cnextfvval  18098  xrsxmet  18842  xrhmeo  18973  cmetcaulem  19243  bcth3  19286  itg2addlem  19652  taylfval  20277  sinord  20438  logexprlim  21011  lgsdir2lem4  21112  hlim2  22696  elnlfn  23433  lnconi  23538  chirredlem3  23897  chirredlem4  23898  cnre2csqlem  24310  subfacp1lem1  24867  prodfn0  25224  prodfrec  25225  prodrblem  25257  fprodcvg  25258  prodmolem2a  25262  wfis3  25492  frins3  25528  wfr2  25557  findreccl  26205  mblfinlem3  26247  mblfinlem4  26248  ismblfin  26249  ftc1anclem3  26284  ftc1anclem8  26289  nn0prpwlem  26327  sdclem2  26448  iscringd  26611  zindbi  27011  fmuldfeq  27691  stoweidlem2  27729  stoweidlem17  27744  stoweidlem21  27748  stoweidlem34  27761  stoweidlem42  27769  stoweidlem43  27770  stoweidlem48  27775  stoweidlem51  27778  wallispi  27797  bnj1321  29458  bnj1418  29471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960
  Copyright terms: Public domain W3C validator