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

Theorem vtoclg 3151
Description: Implicit substitution of a class expression for a setvar 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 nfv 1692 . 2  |-  F/ x ps
2 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
3 vtoclg.2 . 2  |-  ph
41, 2, 3vtoclg1f 3150 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1381    e. wcel 1802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095
This theorem is referenced by:  vtoclbg  3152  moeq3  3260  mo2icl  3262  nelrdva  3293  sbctt  3382  sbcnestgf  3821  csbun  3839  csbin  3842  csbingOLD  3843  csbif  3972  csbifgOLD  3973  prnzg  4131  sneqrg  4180  prel12g  4191  unisng  4246  trss  4535  inex1g  4576  ssexg  4579  pwexg  4617  snex  4674  prex  4675  opth  4707  csbopab  4765  csbopabgALT  4766  ordelord  4886  vtoclr  5030  resieq  5270  csbima12  5340  csbima12gOLD  5341  dmsnsnsn  5472  iota5  5557  csbiota  5566  csbiotagOLD  5567  funmo  5590  funimaexg  5651  fconstg  5758  funbrfv  5892  fvelimab  5910  ssimaexg  5920  fvelrn  6005  isoselem  6218  csbriota  6250  csbov123  6311  csbovgOLD  6313  ovg  6422  caovmo  6493  uniexg  6578  fnse  6898  onfununi  7010  rdg0g  7091  ensn1g  7578  fundmeng  7588  xpdom2g  7611  canth2g  7669  map2xp  7685  mapdom3  7687  php2  7700  canthwdom  8003  elirr  8022  tcvalg  8167  tz9.13g  8208  rankvalg  8233  ranklim  8260  r1pwOLD  8262  rankuni2b  8269  rankuni  8279  cfslb2n  8646  itunitc1  8798  itunitc  8799  ituniiun  8800  hsmex  8810  axdc2lem  8826  ac7g  8852  ac6sg  8866  numthcor  8872  weth  8873  fodomg  8901  pwfseqlem4  9038  pwxpndom2  9041  rankcf  9153  nqereu  9305  prnmax  9371  prlem936  9423  ltord1  10080  xmulasslem  11481  axdc4uz  12067  climshft  13373  telfsumo  13590  fsumparts  13594  mreacs  14927  dprdval  16903  dprdvalOLD  16905  fiinopn  19277  neiptoptop  19498  neiptopnei  19499  pt1hmeo  20173  isfildlem  20224  alexsublem  20410  ustuqtop4  20613  utopsnneiplem  20616  voliunlem3  21828  dvbsss  22172  dvfsumlem2  22294  1pthoncl  24459  sitgclg  28150  mclsrcl  28787  iota5f  28968  shftvalg  28982  dfrdg2  29196  dfpred3g  29223  predbrg  29234  preddowncl  29244  fvsingle  29538  fullfunfv  29565  ranksng  29792  rankelg  29793  rankpwg  29794  rankeq1o  29796  mblfinlem3  30021  ismrer1  30302  mzpclall  30627  mzpcompact2  30653  diophrw  30660  monotuz  30845  monotoddzz  30847  oddcomabszz  30848  divalgmodcl  30897  flcidc  31092  lcmgcdlem  31181  nzss  31191  pm14.122b  31277  sbiota1  31288  monoords  31441  fperiodmullem  31448  0ellimcdiv  31559  cncfperiod  31584  icccncfext  31593  fperdvper  31615  iblspltprt  31658  itgspltprt  31664  stoweidlem4  31671  stoweidlem6  31673  stoweidlem8  31675  stoweidlem15  31682  stoweidlem16  31683  stoweidlem19  31686  stoweidlem20  31687  stoweidlem22  31689  stoweidlem23  31690  stoweidlem27  31694  stoweidlem30  31697  stoweidlem32  31699  stoweidlem34  31701  stoweidlem42  31709  stoweidlem48  31715  fourierdlem11  31785  fourierdlem16  31790  fourierdlem21  31795  fourierdlem41  31815  fourierdlem42  31816  fourierdlem46  31820  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem68  31842  fourierdlem72  31846  fourierdlem76  31850  fourierdlem79  31853  fourierdlem81  31855  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem92  31866  fourierdlem97  31871  fourierdlem103  31877  fourierdlem104  31878  fourierdlem111  31885  csbafv12g  32056  csbaovg  32099
  Copyright terms: Public domain W3C validator