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

Theorem vtoclg 3136
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 1751 . 2  |-  F/ x ps
2 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
3 vtoclg.2 . 2  |-  ph
41, 2, 3vtoclg1f 3135 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-12 1904  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-v 3080
This theorem is referenced by:  vtoclbg  3137  moeq3  3245  mo2icl  3247  nelrdva  3278  sbctt  3359  sbcnestgf  3809  csbun  3823  csbin  3824  csbif  3956  prnzg  4114  sneqrg  4163  prel12g  4174  unisng  4229  trss  4520  inex1g  4559  ssexg  4562  pwexg  4600  snex  4654  prex  4655  opth  4687  csbopab  4744  csbopabgALT  4745  vtoclr  4890  resieq  5126  csbima12  5196  csbima12gOLD  5197  dmsnsnsn  5325  dfpred3g  5401  predbrg  5410  preddowncl  5417  ordelord  5455  iota5  5576  csbiota  5585  funmo  5608  funimaexg  5669  fconstg  5778  funbrfv  5910  fvelimab  5928  ssimaexg  5938  fvelrn  6021  fsn2g  6070  isoselem  6238  csbriota  6270  csbov123  6330  ovg  6440  caovmo  6511  uniexg  6593  fnse  6915  onfununi  7059  rdg0g  7144  ensn1g  7632  fundmeng  7642  xpdom2g  7665  canth2g  7723  map2xp  7739  mapdom3  7741  php2  7754  canthwdom  8085  elirr  8104  tcvalg  8212  tz9.13g  8253  rankvalg  8278  ranklim  8305  r1pwALT  8307  rankuni2b  8314  rankuni  8324  cfslb2n  8687  itunitc1  8839  itunitc  8840  ituniiun  8841  hsmex  8851  axdc2lem  8867  ac7g  8893  ac6sg  8907  numthcor  8913  weth  8914  fodomg  8942  pwfseqlem4  9076  pwxpndom2  9079  rankcf  9191  nqereu  9343  prnmax  9409  prlem936  9461  ltord1  10129  xmulasslem  11560  axdc4uz  12182  relexpind  13095  climshft  13607  telfsumo  13829  fsumparts  13833  lcmgcdlem  14531  mreacs  15508  dprdval  17563  fiinopn  19855  neiptoptop  20071  neiptopnei  20072  pt1hmeo  20745  isfildlem  20796  alexsublem  20983  ustuqtop4  21183  utopsnneiplem  21186  voliunlem3  22379  dvbsss  22731  dvfsumlem2  22853  1pthoncl  25164  acunirnmpt  28098  acunirnmpt2  28099  acunirnmpt2f  28100  carsgsigalem  28973  carsgclctunlem2  28977  carsgclctun  28979  pmeasmono  28982  pmeasadd  28983  sitgclg  29000  mclsrcl  29984  iota5f  30142  shftvalg  30149  dfrdg2  30226  fvsingle  30469  fullfunfv  30496  ranksng  30716  rankelg  30717  rankpwg  30718  rankeq1o  30720  csbdif  31467  mblfinlem3  31683  ismrer1  31874  mzpclall  35278  mzpcompact2  35303  diophrw  35310  monotuz  35499  monotoddzz  35501  oddcomabszz  35502  divalgmodcl  35552  flcidc  35743  csbcog  35884  nzss  36307  pm14.122b  36415  sbiota1  36426  csbingOLD  36859  fiiuncl  37052  monoords  37127  fperiodmullem  37134  0ellimcdiv  37306  cncfperiod  37332  icccncfext  37341  fperdvper  37366  dvnmul  37391  dvnprodlem2  37395  iblspltprt  37423  itgspltprt  37429  stoweidlem4  37437  stoweidlem6  37439  stoweidlem8  37441  stoweidlem15  37448  stoweidlem16  37449  stoweidlem19  37452  stoweidlem20  37453  stoweidlem22  37455  stoweidlem23  37456  stoweidlem27  37460  stoweidlem30  37464  stoweidlem32  37466  stoweidlem34  37468  stoweidlem42  37476  stoweidlem48  37482  fourierdlem11  37553  fourierdlem16  37558  fourierdlem21  37563  fourierdlem41  37583  fourierdlem42  37584  fourierdlem46  37588  fourierdlem48  37590  fourierdlem49  37591  fourierdlem50  37592  fourierdlem68  37610  fourierdlem72  37614  fourierdlem76  37618  fourierdlem79  37621  fourierdlem81  37623  fourierdlem89  37631  fourierdlem90  37632  fourierdlem91  37633  fourierdlem92  37634  fourierdlem97  37639  fourierdlem103  37645  fourierdlem104  37646  fourierdlem111  37653  sge0f1o  37762  sge0p1  37794  csbafv12g  38042  csbaovg  38085
  Copyright terms: Public domain W3C validator