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

Theorem vtoclg 3003
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 2571 . 2  |-  F/_ x A
2 nfv 1629 . 2  |-  F/ x ps
3 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclg.2 . 2  |-  ph
51, 2, 3, 4vtoclgf 3002 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725
This theorem is referenced by:  vtoclbg  3004  ceqex  3058  moeq3  3103  mo2icl  3105  nelrdva  3135  sbctt  3215  sbcnestgf  3290  csbing  3540  csbifg  3759  prnzg  3916  sneqrg  3960  unisng  4024  csbopabg  4275  trss  4303  inex1g  4338  ssexg  4341  pwexg  4375  snex  4397  prex  4398  opth  4427  ordelord  4595  uniexg  4698  vtoclr  4914  resieq  5148  csbima12g  5205  dmsnsnsn  5340  iota5  5430  csbiotag  5439  funmo  5462  funimaexg  5522  fconstg  5622  funbrfv  5757  fvelimab  5774  ssimaexg  5781  fvelrn  5858  isoselem  6053  csbovg  6104  ovg  6204  caovmo  6276  fnse  6455  csbriotag  6554  onfununi  6595  rdg0g  6677  ensn1g  7164  fundmeng  7173  xpdom2g  7196  canth2g  7253  map2xp  7269  mapdom3  7271  php2  7284  canthwdom  7539  elirr  7558  tcvalg  7669  tz9.13g  7710  rankvalg  7735  ranklim  7762  r1pwOLD  7764  rankuni2b  7771  rankuni  7781  cfslb2n  8140  itunitc1  8292  itunitc  8293  ituniiun  8294  hsmex  8304  axdc2lem  8320  ac7g  8346  ac6sg  8360  numthcor  8366  weth  8367  fodomg  8395  pwfseqlem4  8529  pwxpndom2  8532  rankcf  8644  nqereu  8798  prnmax  8864  prlem936  8916  ltord1  9545  xmulasslem  10856  axdc4uz  11314  climshft  12362  fsumtscopo  12573  fsumparts  12577  mreacs  13875  dprdval  15553  fiinopn  16966  neiptoptop  17187  neiptopnei  17188  pt1hmeo  17830  isfildlem  17881  alexsublem  18067  ustuqtop4  18266  utopsnneiplem  18269  voliunlem3  19438  dvbsss  19781  dvfsumlem2  19903  1pthoncl  21584  sitgclg  24648  iota5f  25174  shftvalg  25200  dfrdg2  25415  dfpred3g  25442  predbrg  25453  preddowncl  25463  fvsingle  25757  fullfunfv  25784  ranksng  26100  rankelg  26101  rankpwg  26102  rankeq1o  26104  mblfinlem2  26235  ismrer1  26538  mzpclall  26775  mzpcompact2  26800  diophrw  26808  monotuz  26995  monotoddzz  26997  oddcomabszz  26998  divalgmodcl  27049  flcidc  27347  pm14.122b  27591  sbiota1  27602  stoweidlem4  27720  stoweidlem6  27722  stoweidlem8  27724  stoweidlem15  27731  stoweidlem16  27732  stoweidlem19  27735  stoweidlem20  27736  stoweidlem22  27738  stoweidlem23  27739  stoweidlem27  27743  stoweidlem30  27746  stoweidlem32  27748  csbafv12g  27968  csbaovg  28011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950
  Copyright terms: Public domain W3C validator