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

Theorem vtoclg 2845
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 2421 . 2  |-  F/_ x A
2 nfv 1607 . 2  |-  F/ x ps
3 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclg.2 . 2  |-  ph
51, 2, 3, 4vtoclgf 2844 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1625    e. wcel 1686
This theorem is referenced by:  vtoclbg  2846  ceqex  2900  moeq3  2944  mo2icl  2946  sbctt  3055  sbcnestgf  3130  csbing  3378  csbifg  3595  prnzg  3748  sneqrg  3784  unisng  3846  csbopabg  4096  trss  4124  inex1g  4159  ssexg  4162  pwexg  4196  snex  4218  prex  4219  opth  4247  ordelord  4416  uniexg  4519  vtoclr  4735  resieq  4967  csbima12g  5024  dmsnsnsn  5153  iota5  5241  csbiotag  5250  funmo  5273  funimaexg  5331  fconstg  5430  funbrfv  5563  fvelimab  5580  ssimaexg  5587  fvelrn  5663  isoselem  5840  csbovg  5891  ovg  5988  caovmo  6059  fnse  6234  csbriotag  6319  onfununi  6360  rdg0g  6442  ensn1g  6928  fundmeng  6937  xpdom2g  6960  canth2g  7017  map2xp  7033  mapdom3  7035  php2  7048  canthwdom  7295  elirr  7314  tcvalg  7425  tz9.13g  7466  rankvalg  7491  ranklim  7518  r1pwOLD  7520  rankuni2b  7527  rankuni  7537  cfslb2n  7896  itunitc1  8048  itunitc  8049  ituniiun  8050  hsmex  8060  axdc2lem  8076  ac7g  8103  ac6sg  8117  numthcor  8123  weth  8124  fodomg  8152  pwfseqlem4  8286  pwxpndom2  8289  rankcf  8401  nqereu  8555  prnmax  8621  prlem936  8673  ltord1  9301  xmulasslem  10607  axdc4uz  11047  climshft  12052  fsumtscopo  12262  fsumparts  12266  mreacs  13562  dprdval  15240  fiinopn  16649  pt1hmeo  17499  isfildlem  17554  alexsublem  17740  voliunlem3  18911  dvbsss  19254  dvfsumlem2  19376  dfrdg2  24154  predbrg  24188  preddowncl  24198  fvsingle  24461  funpartfv  24485  fullfunfv  24487  ranksng  24799  rankelg  24800  rankpwg  24801  rankeq1o  24803  prjmapcp2  25181  empklst  26020  ismrer1  26573  mzpclall  26816  mzpcompact2  26841  diophrw  26849  monotuz  27037  monotoddzz  27039  oddcomabszz  27040  divalgmodcl  27091  flcidc  27390  pm14.122b  27634  sbiota1  27645  csbafv12g  28011  csbaovg  28051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792
  Copyright terms: Public domain W3C validator