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

Theorem vtoclg 3406
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 1992 . 2 𝑥𝜓
2 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
3 vtoclg.2 . 2 𝜑
41, 2, 3vtoclg1f 3405 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wcel 2139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-12 2196  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-v 3342
This theorem is referenced by:  vtoclbg  3407  moeq3  3524  mo2icl  3526  nelrdva  3558  sbctt  3641  sbcnestgf  4138  csbun  4152  csbin  4153  csbif  4282  prnzgOLD  4455  sneqrgOLD  4518  prel12gOLD  4531  unisng  4604  trssOLD  4914  inex1g  4953  ssexg  4956  pwexg  4999  snex  5057  prex  5058  opth  5093  csbopab  5158  csbopabgALT  5159  vtoclr  5321  resieq  5565  csbima12  5641  dmsnsnsn  5772  dfpred3g  5852  predbrg  5861  preddowncl  5868  ordelord  5906  iota5  6032  csbiota  6042  funmo  6065  funimaexg  6136  fconstg  6253  funbrfv  6395  fvelimab  6415  ssimaexg  6426  fvelrn  6515  fsn2g  6568  isoselem  6754  csbriota  6786  csbov123  6850  ovg  6964  caovmo  7036  uniexg  7120  fnse  7462  onfununi  7607  rdg0g  7692  ensn1g  8186  fundmeng  8196  xpdom2g  8221  canth2g  8279  map2xp  8295  mapdom3  8297  php2  8310  canthwdom  8649  zfregcl  8664  elirr  8667  tcvalg  8787  tz9.13g  8828  rankvalg  8853  ranklim  8880  r1pwALT  8882  rankuni2b  8889  rankuni  8899  cfslb2n  9282  itunitc1  9434  itunitc  9435  ituniiun  9436  hsmex  9446  axdc2lem  9462  ac7g  9488  ac6sg  9502  numthcor  9508  weth  9509  fodomg  9537  pwfseqlem4  9676  pwxpndom2  9679  rankcf  9791  nqereu  9943  prnmax  10009  prlem936  10061  ltord1  10746  xmulasslem  12308  axdc4uz  12977  relexpind  14003  climshft  14506  telfsumo  14733  fsumparts  14737  lcmgcdlem  15521  mreacs  16520  dprdval  18602  fiinopn  20908  neiptoptop  21137  neiptopnei  21138  pt1hmeo  21811  isfildlem  21862  alexsublem  22049  ustuqtop4  22249  voliunlem3  23520  dvbsss  23865  dvfsumlem2  23989  acunirnmpt  29768  acunirnmpt2  29769  acunirnmpt2f  29770  carsgsigalem  30686  carsgclctunlem2  30690  carsgclctun  30692  pmeasmono  30695  pmeasadd  30696  sitgclg  30713  mclsrcl  31765  iota5f  31913  shftvalg  31924  dfrdg2  32006  fvsingle  32333  fullfunfv  32360  ranksng  32580  rankelg  32581  rankpwg  32582  rankeq1o  32584  csbdif  33482  mblfinlem3  33761  ismrer1  33950  mzpclall  37792  mzpcompact2  37817  diophrw  37824  monotuz  38008  monotoddzz  38010  oddcomabszz  38011  flcidc  38246  csbcog  38443  nzss  39018  pm14.122b  39126  sbiota1  39137  csbingOLD  39554  fiiuncl  39733  axccdom  39915  axccd  39928  monoords  40010  fperiodmullem  40016  0ellimcdiv  40384  cncfperiod  40595  icccncfext  40603  fperdvper  40636  dvnmul  40661  dvnprodlem2  40665  iblspltprt  40692  itgspltprt  40698  stoweidlem4  40724  stoweidlem6  40726  stoweidlem8  40728  stoweidlem15  40735  stoweidlem16  40736  stoweidlem19  40739  stoweidlem20  40740  stoweidlem22  40742  stoweidlem23  40743  stoweidlem27  40747  stoweidlem30  40750  stoweidlem32  40752  stoweidlem34  40754  stoweidlem42  40762  stoweidlem48  40768  fourierdlem11  40838  fourierdlem16  40843  fourierdlem21  40848  fourierdlem41  40868  fourierdlem42  40869  fourierdlem46  40872  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem68  40894  fourierdlem72  40898  fourierdlem76  40902  fourierdlem79  40905  fourierdlem81  40907  fourierdlem89  40915  fourierdlem90  40916  fourierdlem91  40917  fourierdlem92  40918  fourierdlem97  40923  fourierdlem103  40929  fourierdlem104  40930  fourierdlem111  40937  sge0f1o  41102  sge0p1  41134  hoidmvlelem4  41318  smfpimcclem  41519  csbafv12g  41723  csbaovg  41766
  Copyright terms: Public domain W3C validator