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

Theorem vtoclg 2971
Description: Implicit substitution of a class expression for a set 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 nfcv 2540 . 2  |-  F/_ x A
2 nfv 1626 . 2  |-  F/ x ps
3 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclg.2 . 2  |-  ph
51, 2, 3, 4vtoclgf 2970 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721
This theorem is referenced by:  vtoclbg  2972  ceqex  3026  moeq3  3071  mo2icl  3073  nelrdva  3103  sbctt  3183  sbcnestgf  3258  csbing  3508  csbifg  3727  prnzg  3884  sneqrg  3928  unisng  3992  csbopabg  4243  trss  4271  inex1g  4306  ssexg  4309  pwexg  4343  snex  4365  prex  4366  opth  4395  ordelord  4563  uniexg  4665  vtoclr  4881  resieq  5115  csbima12g  5172  dmsnsnsn  5307  iota5  5397  csbiotag  5406  funmo  5429  funimaexg  5489  fconstg  5589  funbrfv  5724  fvelimab  5741  ssimaexg  5748  fvelrn  5825  isoselem  6020  csbovg  6071  ovg  6171  caovmo  6243  fnse  6422  csbriotag  6521  onfununi  6562  rdg0g  6644  ensn1g  7131  fundmeng  7140  xpdom2g  7163  canth2g  7220  map2xp  7236  mapdom3  7238  php2  7251  canthwdom  7503  elirr  7522  tcvalg  7633  tz9.13g  7674  rankvalg  7699  ranklim  7726  r1pwOLD  7728  rankuni2b  7735  rankuni  7745  cfslb2n  8104  itunitc1  8256  itunitc  8257  ituniiun  8258  hsmex  8268  axdc2lem  8284  ac7g  8310  ac6sg  8324  numthcor  8330  weth  8331  fodomg  8359  pwfseqlem4  8493  pwxpndom2  8496  rankcf  8608  nqereu  8762  prnmax  8828  prlem936  8880  ltord1  9509  xmulasslem  10820  axdc4uz  11277  climshft  12325  fsumtscopo  12536  fsumparts  12540  mreacs  13838  dprdval  15516  fiinopn  16929  neiptoptop  17150  neiptopnei  17151  pt1hmeo  17791  isfildlem  17842  alexsublem  18028  ustuqtop4  18227  utopsnneiplem  18230  voliunlem3  19399  dvbsss  19742  dvfsumlem2  19864  1pthoncl  21545  sitgclg  24609  iota5f  25135  shftvalg  25161  dfrdg2  25366  predbrg  25400  preddowncl  25410  fvsingle  25673  fullfunfv  25700  ranksng  26012  rankelg  26013  rankpwg  26014  rankeq1o  26016  mblfinlem2  26144  ismrer1  26437  mzpclall  26674  mzpcompact2  26699  diophrw  26707  monotuz  26894  monotoddzz  26896  oddcomabszz  26897  divalgmodcl  26948  flcidc  27247  pm14.122b  27491  sbiota1  27502  stoweidlem4  27620  stoweidlem6  27622  stoweidlem8  27624  stoweidlem15  27631  stoweidlem16  27632  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem23  27639  stoweidlem27  27643  stoweidlem30  27646  stoweidlem32  27648  csbafv12g  27868  csbaovg  27911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918
  Copyright terms: Public domain W3C validator