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

Theorem vtoclg 3028
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 1673 . 2  |-  F/ x ps
2 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
3 vtoclg.2 . 2  |-  ph
41, 2, 3vtoclg1f 3027 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-v 2972
This theorem is referenced by:  vtoclbg  3029  moeq3  3134  mo2icl  3136  nelrdva  3166  sbctt  3255  sbcnestgf  3689  csbun  3707  csbin  3710  csbingOLD  3711  csbif  3837  csbifgOLD  3838  prnzg  3993  sneqrg  4040  unisng  4105  trss  4392  inex1g  4433  ssexg  4436  pwexg  4474  snex  4531  prex  4532  opth  4564  csbopab  4618  csbopabgALT  4619  ordelord  4739  vtoclr  4881  resieq  5119  csbima12  5184  csbima12gOLD  5185  dmsnsnsn  5315  iota5  5399  csbiota  5408  csbiotagOLD  5409  funmo  5432  funimaexg  5493  fconstg  5595  funbrfv  5728  fvelimab  5745  ssimaexg  5755  fvelrn  5837  isoselem  6030  csbriota  6062  csbov123  6120  csbovgOLD  6122  ovg  6227  caovmo  6298  uniexg  6375  fnse  6687  onfununi  6800  rdg0g  6881  ensn1g  7372  fundmeng  7382  xpdom2g  7405  canth2g  7463  map2xp  7479  mapdom3  7481  php2  7494  canthwdom  7792  elirr  7811  tcvalg  7956  tz9.13g  7997  rankvalg  8022  ranklim  8049  r1pwOLD  8051  rankuni2b  8058  rankuni  8068  cfslb2n  8435  itunitc1  8587  itunitc  8588  ituniiun  8589  hsmex  8599  axdc2lem  8615  ac7g  8641  ac6sg  8655  numthcor  8661  weth  8662  fodomg  8690  pwfseqlem4  8827  pwxpndom2  8830  rankcf  8942  nqereu  9096  prnmax  9162  prlem936  9214  ltord1  9864  xmulasslem  11246  axdc4uz  11803  climshft  13052  fsumtscopo  13263  fsumparts  13267  mreacs  14594  dprdval  16483  dprdvalOLD  16485  fiinopn  18512  neiptoptop  18733  neiptopnei  18734  pt1hmeo  19377  isfildlem  19428  alexsublem  19614  ustuqtop4  19817  utopsnneiplem  19820  voliunlem3  21031  dvbsss  21375  dvfsumlem2  21497  1pthoncl  23489  sitgclg  26726  iota5f  27379  shftvalg  27393  dfrdg2  27607  dfpred3g  27634  predbrg  27645  preddowncl  27655  fvsingle  27949  fullfunfv  27976  ranksng  28203  rankelg  28204  rankpwg  28205  rankeq1o  28207  mblfinlem3  28427  ismrer1  28734  mzpclall  29060  mzpcompact2  29086  diophrw  29094  monotuz  29279  monotoddzz  29281  oddcomabszz  29282  divalgmodcl  29333  flcidc  29528  pm14.122b  29674  sbiota1  29685  stoweidlem4  29796  stoweidlem6  29798  stoweidlem8  29800  stoweidlem15  29807  stoweidlem16  29808  stoweidlem19  29811  stoweidlem20  29812  stoweidlem22  29814  stoweidlem23  29815  stoweidlem27  29819  stoweidlem30  29822  stoweidlem32  29824  stoweidlem34  29826  stoweidlem42  29834  stoweidlem48  29840  csbafv12g  30040  csbaovg  30083
  Copyright terms: Public domain W3C validator