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

Theorem vtoclg 2955
Description: Implicit substitution of a class expression for a set variable. (Contributed by NM, 17-Apr-1995.)
Hypotheses
Ref Expression
vtoclg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtoclg.2  |-  ph
Assertion
Ref Expression
vtoclg  |-  ( A  e.  V  ->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem vtoclg
StepHypRef Expression
1 nfcv 2524 . 2  |-  F/_ x A
2 nfv 1626 . 2  |-  F/ x ps
3 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclg.2 . 2  |-  ph
51, 2, 3, 4vtoclgf 2954 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717
This theorem is referenced by:  vtoclbg  2956  ceqex  3010  moeq3  3055  mo2icl  3057  nelrdva  3087  sbctt  3167  sbcnestgf  3242  csbing  3492  csbifg  3711  prnzg  3868  sneqrg  3911  unisng  3975  csbopabg  4225  trss  4253  inex1g  4288  ssexg  4291  pwexg  4325  snex  4347  prex  4348  opth  4377  ordelord  4545  uniexg  4647  vtoclr  4863  resieq  5097  csbima12g  5154  dmsnsnsn  5289  iota5  5379  csbiotag  5388  funmo  5411  funimaexg  5471  fconstg  5571  funbrfv  5705  fvelimab  5722  ssimaexg  5729  fvelrn  5806  isoselem  6001  csbovg  6052  ovg  6152  caovmo  6224  fnse  6400  csbriotag  6499  onfununi  6540  rdg0g  6622  ensn1g  7109  fundmeng  7118  xpdom2g  7141  canth2g  7198  map2xp  7214  mapdom3  7216  php2  7229  canthwdom  7481  elirr  7500  tcvalg  7611  tz9.13g  7652  rankvalg  7677  ranklim  7704  r1pwOLD  7706  rankuni2b  7713  rankuni  7723  cfslb2n  8082  itunitc1  8234  itunitc  8235  ituniiun  8236  hsmex  8246  axdc2lem  8262  ac7g  8288  ac6sg  8302  numthcor  8308  weth  8309  fodomg  8337  pwfseqlem4  8471  pwxpndom2  8474  rankcf  8586  nqereu  8740  prnmax  8806  prlem936  8858  ltord1  9486  xmulasslem  10797  axdc4uz  11250  climshft  12298  fsumtscopo  12509  fsumparts  12513  mreacs  13811  dprdval  15489  fiinopn  16898  neiptoptop  17119  neiptopnei  17120  pt1hmeo  17760  isfildlem  17811  alexsublem  17997  ustuqtop4  18196  utopsnneiplem  18199  voliunlem3  19314  dvbsss  19657  dvfsumlem2  19779  1pthoncl  21441  iota5f  24962  shftvalg  24988  dfrdg2  25177  predbrg  25211  preddowncl  25221  fvsingle  25484  fullfunfv  25511  ranksng  25823  rankelg  25824  rankpwg  25825  rankeq1o  25827  ismrer1  26239  mzpclall  26476  mzpcompact2  26501  diophrw  26509  monotuz  26696  monotoddzz  26698  oddcomabszz  26699  divalgmodcl  26750  flcidc  27049  pm14.122b  27293  sbiota1  27304  stoweidlem4  27422  stoweidlem6  27424  stoweidlem8  27426  stoweidlem15  27433  stoweidlem16  27434  stoweidlem19  27437  stoweidlem20  27438  stoweidlem22  27440  stoweidlem23  27441  stoweidlem27  27445  stoweidlem30  27448  stoweidlem32  27450  csbafv12g  27671  csbaovg  27714
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902
  Copyright terms: Public domain W3C validator