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

Theorem vtoclg 3568
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 1906 . 2 𝑥𝜓
2 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
3 vtoclg.2 . 2 𝜑
41, 2, 3vtoclg1f 3567 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-cleq 2814  df-clel 2893
This theorem is referenced by:  vtoclbg  3569  vtocl2g  3572  vtoclga  3574  nelrdva  3695  moeq3  3702  mo2icl  3704  sbctt  3843  sbcnestgfw  4369  sbcnestgf  4374  csbun  4389  csbin  4390  csbif  4520  inex1g  5215  ssexg  5219  pwexg  5271  snex  5323  prex  5324  opth  5360  csbopab  5434  csbopabgALT  5435  vtoclr  5609  resieq  5858  csbima12  5941  dmsnsnsn  6071  dfpred3g  6153  predbrg  6162  preddowncl  6169  ordelord  6207  iota5  6332  csbiota  6342  funmo  6365  funimaexg  6434  fconstg  6560  funbrfv  6710  fvelimab  6731  ssimaexg  6743  fvelrn  6837  isoselem  7083  csbriota  7118  csbov123  7187  ovg  7302  caovmo  7374  uniexg  7456  fnse  7818  onfununi  7969  rdg0g  8054  ensn1g  8563  fundmeng  8573  xpdom2g  8602  canth2g  8660  php2  8691  canthwdom  9032  zfregcl  9047  elirr  9050  tcvalg  9169  tz9.13g  9210  rankvalg  9235  ranklim  9262  r1pwALT  9264  rankuni2b  9271  rankuni  9281  cfslb2n  9679  itunitc1  9831  itunitc  9832  ituniiun  9833  hsmex  9843  axdc2lem  9859  ac7g  9885  ac6sg  9899  numthcor  9905  weth  9906  fodomg  9934  pwfseqlem4  10073  rankcf  10188  nqereu  10340  prnmax  10406  prlem936  10458  ltord1  11155  xmulasslem  12668  axdc4uz  13342  relexpind  14413  climshft  14923  telfsumo  15147  fsumparts  15151  lcmgcdlem  15940  mreacs  16919  dprdval  19056  fiinopn  21439  neiptoptop  21669  neiptopnei  21670  pt1hmeo  22344  isfildlem  22395  alexsublem  22582  ustuqtop4  22782  voliunlem3  24082  dvbsss  24429  dvfsumlem2  24553  acunirnmpt  30333  acunirnmpt2  30334  acunirnmpt2f  30335  carsgsigalem  31473  carsgclctunlem2  31477  carsgclctun  31479  pmeasmono  31482  pmeasadd  31483  sitgclg  31500  mclsrcl  32706  iota5f  32853  shftvalg  32861  dfrdg2  32938  fvsingle  33279  fullfunfv  33306  ranksng  33526  rankelg  33527  rankpwg  33528  rankeq1o  33530  csbdif  34489  mblfinlem3  34813  ismrer1  34999  mzpclall  39204  mzpcompact2  39229  diophrw  39236  monotuz  39418  monotoddzz  39420  oddcomabszz  39421  flcidc  39654  csbcog  39874  nzss  40529  pm14.122b  40635  sbiota1  40646  fiiuncl  41207  axccdom  41367  axccd  41375  monoords  41444  fperiodmullem  41450  0ellimcdiv  41810  cncfperiod  42042  icccncfext  42050  fperdvper  42083  dvnmul  42108  dvnprodlem2  42112  iblspltprt  42138  itgspltprt  42144  stoweidlem4  42170  stoweidlem6  42172  stoweidlem8  42174  stoweidlem15  42181  stoweidlem16  42182  stoweidlem19  42185  stoweidlem20  42186  stoweidlem22  42188  stoweidlem23  42189  stoweidlem27  42193  stoweidlem30  42196  stoweidlem32  42198  stoweidlem34  42200  stoweidlem42  42208  stoweidlem48  42214  fourierdlem11  42284  fourierdlem16  42289  fourierdlem21  42294  fourierdlem41  42314  fourierdlem42  42315  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem68  42340  fourierdlem72  42344  fourierdlem76  42348  fourierdlem79  42351  fourierdlem81  42353  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem92  42364  fourierdlem97  42369  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  sge0f1o  42545  sge0p1  42577  hoidmvlelem4  42761  smfpimcclem  42962  funressnmo  43162  aiota0def  43175  csbafv12g  43217  csbaovg  43260  csbafv212g  43299  funressndmafv2rn  43303  funressnbrafv2  43324  funbrafv2  43327
  Copyright terms: Public domain W3C validator