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

Theorem vtoclg 3119
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 1772 . 2  |-  F/ x ps
2 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
3 vtoclg.2 . 2  |-  ph
41, 2, 3vtoclg1f 3118 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455    e. wcel 1898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059
This theorem is referenced by:  vtoclbg  3120  moeq3  3227  mo2icl  3229  nelrdva  3261  sbctt  3342  sbcnestgf  3796  csbun  3810  csbin  3811  csbif  3943  prnzg  4105  sneqrg  4154  prel12g  4169  unisng  4228  trss  4520  inex1g  4560  ssexg  4563  pwexg  4601  snex  4655  prex  4656  opth  4690  csbopab  4747  csbopabgALT  4748  vtoclr  4898  resieq  5134  csbima12  5204  csbima12gOLD  5205  dmsnsnsn  5333  dfpred3g  5410  predbrg  5419  preddowncl  5426  ordelord  5464  iota5  5585  csbiota  5594  funmo  5617  funimaexg  5682  fconstg  5793  funbrfv  5926  fvelimab  5944  ssimaexg  5954  fvelrn  6038  fsn2g  6088  isoselem  6257  csbriota  6289  csbov123  6349  ovg  6462  caovmo  6533  uniexg  6615  fnse  6940  onfununi  7086  rdg0g  7171  ensn1g  7660  fundmeng  7670  xpdom2g  7694  canth2g  7752  map2xp  7768  mapdom3  7770  php2  7783  canthwdom  8120  elirr  8139  tcvalg  8248  tz9.13g  8289  rankvalg  8314  ranklim  8341  r1pwALT  8343  rankuni2b  8350  rankuni  8360  cfslb2n  8724  itunitc1  8876  itunitc  8877  ituniiun  8878  hsmex  8888  axdc2lem  8904  ac7g  8930  ac6sg  8944  numthcor  8950  weth  8951  fodomg  8979  pwfseqlem4  9113  pwxpndom2  9116  rankcf  9228  nqereu  9380  prnmax  9446  prlem936  9498  ltord1  10168  xmulasslem  11600  axdc4uz  12228  relexpind  13176  climshft  13689  telfsumo  13911  fsumparts  13915  lcmgcdlem  14620  mreacs  15613  dprdval  17684  fiinopn  19980  neiptoptop  20196  neiptopnei  20197  pt1hmeo  20870  isfildlem  20921  alexsublem  21108  ustuqtop4  21308  utopsnneiplem  21311  voliunlem3  22554  dvbsss  22906  dvfsumlem2  23028  1pthoncl  25371  acunirnmpt  28310  acunirnmpt2  28311  acunirnmpt2f  28312  carsgsigalem  29196  carsgclctunlem2  29200  carsgclctun  29202  pmeasmono  29206  pmeasadd  29207  sitgclg  29224  mclsrcl  30248  iota5f  30406  shftvalg  30414  dfrdg2  30491  fvsingle  30736  fullfunfv  30763  ranksng  30983  rankelg  30984  rankpwg  30985  rankeq1o  30987  csbdif  31771  mblfinlem3  32024  ismrer1  32215  mzpclall  35614  mzpcompact2  35639  diophrw  35646  monotuz  35834  monotoddzz  35836  oddcomabszz  35837  divalgmodcl  35887  flcidc  36085  csbcog  36286  nzss  36710  pm14.122b  36818  sbiota1  36829  csbingOLD  37255  fiiuncl  37444  monoords  37552  fperiodmullem  37559  0ellimcdiv  37768  cncfperiod  37794  icccncfext  37803  fperdvper  37828  dvnmul  37856  dvnprodlem2  37860  iblspltprt  37888  itgspltprt  37894  stoweidlem4  37902  stoweidlem6  37904  stoweidlem8  37906  stoweidlem15  37913  stoweidlem16  37914  stoweidlem19  37917  stoweidlem20  37918  stoweidlem22  37920  stoweidlem23  37921  stoweidlem27  37925  stoweidlem30  37929  stoweidlem32  37931  stoweidlem34  37933  stoweidlem42  37941  stoweidlem48  37947  fourierdlem11  38018  fourierdlem16  38023  fourierdlem21  38028  fourierdlem41  38049  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem46  38054  fourierdlem48  38056  fourierdlem49  38057  fourierdlem50  38058  fourierdlem68  38076  fourierdlem72  38080  fourierdlem76  38084  fourierdlem79  38087  fourierdlem81  38089  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem92  38100  fourierdlem97  38105  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  sge0f1o  38262  sge0p1  38294  hoidmvlelem4  38458  csbafv12g  38677  csbaovg  38720
  Copyright terms: Public domain W3C validator