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

Theorem vtoclg 3167
Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
Hypotheses
Ref Expression
vtoclg.1
vtoclg.2
Assertion
Ref Expression
vtoclg
Distinct variable groups:   ,   ,

Proof of Theorem vtoclg
StepHypRef Expression
1 nfv 1707 . 2
2 vtoclg.1 . 2
3 vtoclg.2 . 2
41, 2, 3vtoclg1f 3166 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  vtoclbg  3168  moeq3  3276  mo2icl  3278  nelrdva  3309  sbctt  3398  sbcnestgf  3839  csbun  3857  csbin  3860  csbingOLD  3861  csbif  3991  csbifgOLD  3992  prnzg  4150  sneqrg  4199  prel12g  4210  unisng  4265  trss  4554  inex1g  4595  ssexg  4598  pwexg  4636  snex  4693  prex  4694  opth  4726  csbopab  4784  csbopabgALT  4785  ordelord  4905  vtoclr  5049  resieq  5289  csbima12  5359  csbima12gOLD  5360  dmsnsnsn  5491  iota5  5576  csbiota  5585  csbiotagOLD  5586  funmo  5609  funimaexg  5670  fconstg  5777  funbrfv  5911  fvelimab  5929  ssimaexg  5939  fvelrn  6024  isoselem  6237  csbriota  6269  csbov123  6330  csbovgOLD  6332  ovg  6441  caovmo  6512  uniexg  6597  fnse  6917  onfununi  7031  rdg0g  7112  ensn1g  7600  fundmeng  7610  xpdom2g  7633  canth2g  7691  map2xp  7707  mapdom3  7709  php2  7722  canthwdom  8026  elirr  8045  tcvalg  8190  tz9.13g  8231  rankvalg  8256  ranklim  8283  r1pwOLD  8285  rankuni2b  8292  rankuni  8302  cfslb2n  8669  itunitc1  8821  itunitc  8822  ituniiun  8823  hsmex  8833  axdc2lem  8849  ac7g  8875  ac6sg  8889  numthcor  8895  weth  8896  fodomg  8924  pwfseqlem4  9061  pwxpndom2  9064  rankcf  9176  nqereu  9328  prnmax  9394  prlem936  9446  ltord1  10104  xmulasslem  11506  axdc4uz  12093  climshft  13399  telfsumo  13616  fsumparts  13620  mreacs  15055  dprdval  17034  dprdvalOLD  17036  fiinopn  19410  neiptoptop  19632  neiptopnei  19633  pt1hmeo  20307  isfildlem  20358  alexsublem  20544  ustuqtop4  20747  utopsnneiplem  20750  voliunlem3  21962  dvbsss  22306  dvfsumlem2  22428  1pthoncl  24594  sitgclg  28284  mclsrcl  28921  iota5f  29102  shftvalg  29115  dfrdg2  29228  dfpred3g  29255  predbrg  29266  preddowncl  29276  fvsingle  29570  fullfunfv  29597  ranksng  29824  rankelg  29825  rankpwg  29826  rankeq1o  29828  mblfinlem3  30053  ismrer1  30334  mzpclall  30659  mzpcompact2  30685  diophrw  30692  monotuz  30877  monotoddzz  30879  oddcomabszz  30880  divalgmodcl  30929  flcidc  31123  lcmgcdlem  31212  nzss  31222  pm14.122b  31330  sbiota1  31341  monoords  31496  fperiodmullem  31503  0ellimcdiv  31655  cncfperiod  31681  icccncfext  31690  fperdvper  31715  dvnmul  31740  dvnprodlem2  31744  iblspltprt  31772  itgspltprt  31778  stoweidlem4  31786  stoweidlem6  31788  stoweidlem8  31790  stoweidlem15  31797  stoweidlem16  31798  stoweidlem19  31801  stoweidlem20  31802  stoweidlem22  31804  stoweidlem23  31805  stoweidlem27  31809  stoweidlem30  31812  stoweidlem32  31814  stoweidlem34  31816  stoweidlem42  31824  stoweidlem48  31830  fourierdlem11  31900  fourierdlem16  31905  fourierdlem21  31910  fourierdlem41  31930  fourierdlem42  31931  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem68  31957  fourierdlem72  31961  fourierdlem76  31965  fourierdlem79  31968  fourierdlem81  31970  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  csbafv12g  32222  csbaovg  32265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator