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 1678 . 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 1374    e. wcel 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-v 3108
This theorem is referenced by:  vtoclbg  3165  moeq3  3273  mo2icl  3275  nelrdva  3306  sbctt  3395  sbcnestgf  3832  csbun  3850  csbin  3853  csbingOLD  3854  csbif  3982  csbifgOLD  3983  prnzg  4140  sneqrg  4189  unisng  4254  trss  4542  inex1g  4583  ssexg  4586  pwexg  4624  snex  4681  prex  4682  opth  4714  csbopab  4772  csbopabgALT  4773  ordelord  4893  vtoclr  5036  resieq  5275  csbima12  5345  csbima12gOLD  5346  dmsnsnsn  5477  iota5  5562  csbiota  5571  csbiotagOLD  5572  funmo  5595  funimaexg  5656  fconstg  5763  funbrfv  5897  fvelimab  5914  ssimaexg  5924  fvelrn  6008  isoselem  6216  csbriota  6248  csbov123  6306  csbovgOLD  6308  ovg  6416  caovmo  6487  uniexg  6572  fnse  6890  onfununi  7002  rdg0g  7083  ensn1g  7570  fundmeng  7580  xpdom2g  7603  canth2g  7661  map2xp  7677  mapdom3  7679  php2  7692  canthwdom  7994  elirr  8013  tcvalg  8158  tz9.13g  8199  rankvalg  8224  ranklim  8251  r1pwOLD  8253  rankuni2b  8260  rankuni  8270  cfslb2n  8637  itunitc1  8789  itunitc  8790  ituniiun  8791  hsmex  8801  axdc2lem  8817  ac7g  8843  ac6sg  8857  numthcor  8863  weth  8864  fodomg  8892  pwfseqlem4  9029  pwxpndom2  9032  rankcf  9144  nqereu  9296  prnmax  9362  prlem936  9414  ltord1  10068  xmulasslem  11466  axdc4uz  12049  climshft  13348  telfsumo  13565  fsumparts  13569  mreacs  14902  dprdval  16818  dprdvalOLD  16820  fiinopn  19170  neiptoptop  19391  neiptopnei  19392  pt1hmeo  20035  isfildlem  20086  alexsublem  20272  ustuqtop4  20475  utopsnneiplem  20478  voliunlem3  21690  dvbsss  22034  dvfsumlem2  22156  1pthoncl  24256  sitgclg  27910  iota5f  28563  shftvalg  28577  dfrdg2  28791  dfpred3g  28818  predbrg  28829  preddowncl  28839  fvsingle  29133  fullfunfv  29160  ranksng  29387  rankelg  29388  rankpwg  29389  rankeq1o  29391  mblfinlem3  29617  ismrer1  29924  mzpclall  30250  mzpcompact2  30276  diophrw  30283  monotuz  30468  monotoddzz  30470  oddcomabszz  30471  divalgmodcl  30522  flcidc  30717  pm14.122b  30863  sbiota1  30874  monoords  31028  fperiodmullem  31035  0ellimcdiv  31146  stoweidlem4  31259  stoweidlem6  31261  stoweidlem8  31263  stoweidlem15  31270  stoweidlem16  31271  stoweidlem19  31274  stoweidlem20  31275  stoweidlem22  31277  stoweidlem23  31278  stoweidlem27  31282  stoweidlem30  31285  stoweidlem32  31287  stoweidlem34  31289  stoweidlem42  31297  stoweidlem48  31303  fourierdlem16  31378  fourierdlem21  31383  fourierdlem41  31403  fourierdlem42  31404  fourierdlem46  31408  fourierdlem48  31410  fourierdlem49  31411  fourierdlem50  31412  fourierdlem51  31413  fourierdlem68  31430  fourierdlem71  31433  fourierdlem76  31438  fourierdlem79  31441  fourierdlem89  31451  fourierdlem90  31452  fourierdlem91  31453  fourierdlem97  31459  fourierdlem103  31465  fourierdlem104  31466  fourierdlem111  31473  csbafv12g  31644  csbaovg  31687
  Copyright terms: Public domain W3C validator