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

Theorem vtoclg 3238
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 1829 . 2 𝑥𝜓
2 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
3 vtoclg.2 . 2 𝜑
41, 2, 3vtoclg1f 3237 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174
This theorem is referenced by:  vtoclbg  3239  moeq3  3349  mo2icl  3351  nelrdva  3383  sbctt  3466  sbcnestgf  3946  csbun  3960  csbin  3961  csbif  4087  prnzgOLD  4254  sneqrgOLD  4308  prel12g  4322  unisng  4382  trssOLD  4684  inex1g  4724  ssexg  4727  pwexg  4771  snex  4830  prex  4831  opth  4865  csbopab  4922  csbopabgALT  4923  vtoclr  5076  resieq  5314  csbima12  5389  dmsnsnsn  5517  dfpred3g  5594  predbrg  5603  preddowncl  5610  ordelord  5648  iota5  5774  csbiota  5783  funmo  5806  funimaexg  5875  fconstg  5990  funbrfv  6129  fvelimab  6148  ssimaexg  6159  fvelrn  6245  fsn2g  6296  isoselem  6469  csbriota  6501  csbov123  6563  ovg  6675  caovmo  6746  uniexg  6830  fnse  7158  onfununi  7302  rdg0g  7387  ensn1g  7884  fundmeng  7894  xpdom2g  7918  canth2g  7976  map2xp  7992  mapdom3  7994  php2  8007  canthwdom  8344  zfregcl  8359  elirr  8365  tcvalg  8474  tz9.13g  8515  rankvalg  8540  ranklim  8567  r1pwALT  8569  rankuni2b  8576  rankuni  8586  cfslb2n  8950  itunitc1  9102  itunitc  9103  ituniiun  9104  hsmex  9114  axdc2lem  9130  ac7g  9156  ac6sg  9170  numthcor  9176  weth  9177  fodomg  9205  pwfseqlem4  9340  pwxpndom2  9343  rankcf  9455  nqereu  9607  prnmax  9673  prlem936  9725  ltord1  10403  xmulasslem  11944  axdc4uz  12600  relexpind  13598  climshft  14101  telfsumo  14321  fsumparts  14325  lcmgcdlem  15103  mreacs  16088  dprdval  18171  fiinopn  20473  neiptoptop  20687  neiptopnei  20688  pt1hmeo  21361  isfildlem  21413  alexsublem  21600  ustuqtop4  21800  voliunlem3  23044  dvbsss  23389  dvfsumlem2  23511  1pthoncl  25888  acunirnmpt  28647  acunirnmpt2  28648  acunirnmpt2f  28649  carsgsigalem  29510  carsgclctunlem2  29514  carsgclctun  29516  pmeasmono  29519  pmeasadd  29520  sitgclg  29537  mclsrcl  30518  iota5f  30667  shftvalg  30676  dfrdg2  30751  fvsingle  31003  fullfunfv  31030  ranksng  31250  rankelg  31251  rankpwg  31252  rankeq1o  31254  csbdif  32143  mblfinlem3  32414  ismrer1  32603  mzpclall  36104  mzpcompact2  36129  diophrw  36136  monotuz  36320  monotoddzz  36322  oddcomabszz  36323  flcidc  36559  csbcog  36756  nzss  37334  pm14.122b  37442  sbiota1  37453  csbingOLD  37872  fiiuncl  38055  axccdom  38207  axccd  38220  monoords  38248  fperiodmullem  38254  0ellimcdiv  38513  cncfperiod  38561  icccncfext  38570  fperdvper  38605  dvnmul  38630  dvnprodlem2  38634  iblspltprt  38662  itgspltprt  38668  stoweidlem4  38694  stoweidlem6  38696  stoweidlem8  38698  stoweidlem15  38705  stoweidlem16  38706  stoweidlem19  38709  stoweidlem20  38710  stoweidlem22  38712  stoweidlem23  38713  stoweidlem27  38717  stoweidlem30  38720  stoweidlem32  38722  stoweidlem34  38724  stoweidlem42  38732  stoweidlem48  38738  fourierdlem11  38808  fourierdlem16  38813  fourierdlem21  38818  fourierdlem41  38838  fourierdlem42  38839  fourierdlem46  38842  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem68  38864  fourierdlem72  38868  fourierdlem76  38872  fourierdlem79  38875  fourierdlem81  38877  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem92  38888  fourierdlem97  38893  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  sge0f1o  39072  sge0p1  39104  hoidmvlelem4  39285  csbafv12g  39664  csbaovg  39707
  Copyright terms: Public domain W3C validator