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

Theorem vtoclg 3164
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 1712 . 2  |-  F/ x ps
2 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
3 vtoclg.2 . 2  |-  ph
41, 2, 3vtoclg1f 3163 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398    e. wcel 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108
This theorem is referenced by:  vtoclbg  3165  moeq3  3273  mo2icl  3275  nelrdva  3306  sbctt  3387  sbcnestgf  3834  csbun  3848  csbin  3849  csbif  3979  prnzg  4136  sneqrg  4185  prel12g  4196  unisng  4251  trss  4541  inex1g  4580  ssexg  4583  pwexg  4621  snex  4678  prex  4679  opth  4711  csbopab  4768  csbopabgALT  4769  ordelord  4889  vtoclr  5033  resieq  5272  csbima12  5342  csbima12gOLD  5343  dmsnsnsn  5469  iota5  5554  csbiota  5563  funmo  5586  funimaexg  5647  fconstg  5754  funbrfv  5886  fvelimab  5904  ssimaexg  5914  fvelrn  6000  isoselem  6212  csbriota  6244  csbov123  6304  ovg  6414  caovmo  6485  uniexg  6570  fnse  6890  onfununi  7004  rdg0g  7085  ensn1g  7573  fundmeng  7583  xpdom2g  7606  canth2g  7664  map2xp  7680  mapdom3  7682  php2  7695  canthwdom  7997  elirr  8016  tcvalg  8160  tz9.13g  8201  rankvalg  8226  ranklim  8253  r1pwALT  8255  rankuni2b  8262  rankuni  8272  cfslb2n  8639  itunitc1  8791  itunitc  8792  ituniiun  8793  hsmex  8803  axdc2lem  8819  ac7g  8845  ac6sg  8859  numthcor  8865  weth  8866  fodomg  8894  pwfseqlem4  9029  pwxpndom2  9032  rankcf  9144  nqereu  9296  prnmax  9362  prlem936  9414  ltord1  10075  xmulasslem  11480  axdc4uz  12075  relexpind  12979  climshft  13481  telfsumo  13698  fsumparts  13702  mreacs  15147  dprdval  17229  dprdvalOLD  17231  fiinopn  19577  neiptoptop  19799  neiptopnei  19800  pt1hmeo  20473  isfildlem  20524  alexsublem  20710  ustuqtop4  20913  utopsnneiplem  20916  voliunlem3  22128  dvbsss  22472  dvfsumlem2  22594  1pthoncl  24796  acunirnmpt  27726  acunirnmpt2  27727  acunirnmpt2f  27728  carsgsigalem  28523  carsgclctunlem2  28527  carsgclctun  28529  sitgclg  28548  mclsrcl  29185  iota5f  29343  shftvalg  29356  dfrdg2  29468  dfpred3g  29495  predbrg  29506  preddowncl  29516  fvsingle  29798  fullfunfv  29825  ranksng  30052  rankelg  30053  rankpwg  30054  rankeq1o  30056  mblfinlem3  30293  ismrer1  30574  mzpclall  30899  mzpcompact2  30924  diophrw  30931  monotuz  31116  monotoddzz  31118  oddcomabszz  31119  divalgmodcl  31168  flcidc  31364  lcmgcdlem  31453  nzss  31463  pm14.122b  31571  sbiota1  31582  monoords  31735  fperiodmullem  31742  0ellimcdiv  31894  cncfperiod  31920  icccncfext  31929  fperdvper  31954  dvnmul  31979  dvnprodlem2  31983  iblspltprt  32011  itgspltprt  32017  stoweidlem4  32025  stoweidlem6  32027  stoweidlem8  32029  stoweidlem15  32036  stoweidlem16  32037  stoweidlem19  32040  stoweidlem20  32041  stoweidlem22  32043  stoweidlem23  32044  stoweidlem27  32048  stoweidlem30  32051  stoweidlem32  32053  stoweidlem34  32055  stoweidlem42  32063  stoweidlem48  32069  fourierdlem11  32139  fourierdlem16  32144  fourierdlem21  32149  fourierdlem41  32169  fourierdlem42  32170  fourierdlem46  32174  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem68  32196  fourierdlem72  32200  fourierdlem76  32204  fourierdlem79  32207  fourierdlem81  32209  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem92  32220  fourierdlem97  32225  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  csbafv12g  32461  csbaovg  32504  csbingOLD  34019
  Copyright terms: Public domain W3C validator