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

Theorem vtoclg 3297
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 1883 . 2 𝑥𝜓
2 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
3 vtoclg.2 . 2 𝜑
41, 2, 3vtoclg1f 3296 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  vtoclbg  3298  moeq3  3416  mo2icl  3418  nelrdva  3450  sbctt  3533  sbcnestgf  4028  csbun  4042  csbin  4043  csbif  4171  prnzgOLD  4343  sneqrgOLD  4405  prel12g  4418  unisng  4484  trssOLD  4795  inex1g  4834  ssexg  4837  pwexg  4880  snex  4938  prex  4939  opth  4974  csbopab  5037  csbopabgALT  5038  vtoclr  5198  resieq  5442  csbima12  5518  dmsnsnsn  5649  dfpred3g  5729  predbrg  5738  preddowncl  5745  ordelord  5783  iota5  5909  csbiota  5919  funmo  5942  funimaexg  6013  fconstg  6130  funbrfv  6272  fvelimab  6292  ssimaexg  6303  fvelrn  6392  fsn2g  6445  isoselem  6631  csbriota  6663  csbov123  6727  ovg  6841  caovmo  6913  uniexg  6997  fnse  7339  onfununi  7483  rdg0g  7568  ensn1g  8062  fundmeng  8072  xpdom2g  8097  canth2g  8155  map2xp  8171  mapdom3  8173  php2  8186  canthwdom  8525  zfregcl  8540  elirr  8543  tcvalg  8652  tz9.13g  8693  rankvalg  8718  ranklim  8745  r1pwALT  8747  rankuni2b  8754  rankuni  8764  cfslb2n  9128  itunitc1  9280  itunitc  9281  ituniiun  9282  hsmex  9292  axdc2lem  9308  ac7g  9334  ac6sg  9348  numthcor  9354  weth  9355  fodomg  9383  pwfseqlem4  9522  pwxpndom2  9525  rankcf  9637  nqereu  9789  prnmax  9855  prlem936  9907  ltord1  10592  xmulasslem  12153  axdc4uz  12823  relexpind  13848  climshft  14351  telfsumo  14578  fsumparts  14582  lcmgcdlem  15366  mreacs  16366  dprdval  18448  fiinopn  20754  neiptoptop  20983  neiptopnei  20984  pt1hmeo  21657  isfildlem  21708  alexsublem  21895  ustuqtop4  22095  voliunlem3  23366  dvbsss  23711  dvfsumlem2  23835  acunirnmpt  29587  acunirnmpt2  29588  acunirnmpt2f  29589  carsgsigalem  30505  carsgclctunlem2  30509  carsgclctun  30511  pmeasmono  30514  pmeasadd  30515  sitgclg  30532  mclsrcl  31584  iota5f  31732  shftvalg  31743  dfrdg2  31825  fvsingle  32152  fullfunfv  32179  ranksng  32399  rankelg  32400  rankpwg  32401  rankeq1o  32403  csbdif  33301  mblfinlem3  33578  ismrer1  33767  mzpclall  37607  mzpcompact2  37632  diophrw  37639  monotuz  37823  monotoddzz  37825  oddcomabszz  37826  flcidc  38061  csbcog  38258  nzss  38833  pm14.122b  38941  sbiota1  38952  csbingOLD  39369  fiiuncl  39548  axccdom  39730  axccd  39743  monoords  39825  fperiodmullem  39831  0ellimcdiv  40199  cncfperiod  40410  icccncfext  40418  fperdvper  40451  dvnmul  40476  dvnprodlem2  40480  iblspltprt  40507  itgspltprt  40513  stoweidlem4  40539  stoweidlem6  40541  stoweidlem8  40543  stoweidlem15  40550  stoweidlem16  40551  stoweidlem19  40554  stoweidlem20  40555  stoweidlem22  40557  stoweidlem23  40558  stoweidlem27  40562  stoweidlem30  40565  stoweidlem32  40567  stoweidlem34  40569  stoweidlem42  40577  stoweidlem48  40583  fourierdlem11  40653  fourierdlem16  40658  fourierdlem21  40663  fourierdlem41  40683  fourierdlem42  40684  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem68  40709  fourierdlem72  40713  fourierdlem76  40717  fourierdlem79  40720  fourierdlem81  40722  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  sge0f1o  40917  sge0p1  40949  hoidmvlelem4  41133  smfpimcclem  41334  csbafv12g  41538  csbaovg  41581
  Copyright terms: Public domain W3C validator