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

Theorem vtoclg 3256
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:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg
StepHypRef Expression
1 nfv 1840 . 2 𝑥𝜓
2 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
3 vtoclg.2 . 2 𝜑
41, 2, 3vtoclg1f 3255 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3192
This theorem is referenced by:  vtoclbg  3257  moeq3  3370  mo2icl  3372  nelrdva  3404  sbctt  3487  sbcnestgf  3973  csbun  3987  csbin  3988  csbif  4116  prnzgOLD  4289  sneqrgOLD  4348  prel12g  4362  unisng  4425  trssOLD  4732  inex1g  4771  ssexg  4774  pwexg  4820  snex  4879  prex  4880  opth  4915  csbopab  4978  csbopabgALT  4979  vtoclr  5134  resieq  5376  csbima12  5452  dmsnsnsn  5582  dfpred3g  5660  predbrg  5669  preddowncl  5676  ordelord  5714  iota5  5840  csbiota  5850  funmo  5873  funimaexg  5943  fconstg  6059  funbrfv  6201  fvelimab  6220  ssimaexg  6231  fvelrn  6318  fsn2g  6370  isoselem  6556  csbriota  6588  csbov123  6652  ovg  6764  caovmo  6836  uniexg  6920  fnse  7254  onfununi  7398  rdg0g  7483  ensn1g  7981  fundmeng  7991  xpdom2g  8016  canth2g  8074  map2xp  8090  mapdom3  8092  php2  8105  canthwdom  8444  zfregcl  8459  elirr  8465  tcvalg  8574  tz9.13g  8615  rankvalg  8640  ranklim  8667  r1pwALT  8669  rankuni2b  8676  rankuni  8686  cfslb2n  9050  itunitc1  9202  itunitc  9203  ituniiun  9204  hsmex  9214  axdc2lem  9230  ac7g  9256  ac6sg  9270  numthcor  9276  weth  9277  fodomg  9305  pwfseqlem4  9444  pwxpndom2  9447  rankcf  9559  nqereu  9711  prnmax  9777  prlem936  9829  ltord1  10514  xmulasslem  12074  axdc4uz  12739  relexpind  13754  climshft  14257  telfsumo  14480  fsumparts  14484  lcmgcdlem  15262  mreacs  16259  dprdval  18342  fiinopn  20646  neiptoptop  20875  neiptopnei  20876  pt1hmeo  21549  isfildlem  21601  alexsublem  21788  ustuqtop4  21988  voliunlem3  23260  dvbsss  23606  dvfsumlem2  23728  acunirnmpt  29342  acunirnmpt2  29343  acunirnmpt2f  29344  carsgsigalem  30200  carsgclctunlem2  30204  carsgclctun  30206  pmeasmono  30209  pmeasadd  30210  sitgclg  30227  mclsrcl  31219  iota5f  31368  shftvalg  31378  dfrdg2  31455  fvsingle  31722  fullfunfv  31749  ranksng  31969  rankelg  31970  rankpwg  31971  rankeq1o  31973  csbdif  32842  mblfinlem3  33119  ismrer1  33308  mzpclall  36809  mzpcompact2  36834  diophrw  36841  monotuz  37025  monotoddzz  37027  oddcomabszz  37028  flcidc  37264  csbcog  37461  nzss  38037  pm14.122b  38145  sbiota1  38156  csbingOLD  38576  fiiuncl  38756  axccdom  38925  axccd  38938  monoords  39010  fperiodmullem  39016  0ellimcdiv  39317  cncfperiod  39427  icccncfext  39435  fperdvper  39470  dvnmul  39495  dvnprodlem2  39499  iblspltprt  39526  itgspltprt  39532  stoweidlem4  39558  stoweidlem6  39560  stoweidlem8  39562  stoweidlem15  39569  stoweidlem16  39570  stoweidlem19  39573  stoweidlem20  39574  stoweidlem22  39576  stoweidlem23  39577  stoweidlem27  39581  stoweidlem30  39584  stoweidlem32  39586  stoweidlem34  39588  stoweidlem42  39596  stoweidlem48  39602  fourierdlem11  39672  fourierdlem16  39677  fourierdlem21  39682  fourierdlem41  39702  fourierdlem42  39703  fourierdlem46  39706  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem68  39728  fourierdlem72  39732  fourierdlem76  39736  fourierdlem79  39739  fourierdlem81  39741  fourierdlem89  39749  fourierdlem90  39750  fourierdlem91  39751  fourierdlem92  39752  fourierdlem97  39757  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  sge0f1o  39936  sge0p1  39968  hoidmvlelem4  40149  smfpimcclem  40350  csbafv12g  40551  csbaovg  40594
  Copyright terms: Public domain W3C validator