Theorem vtoclg 3524

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2216. (Revised by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 26-Jan-2025.)

Hypotheses

Ref	Expression
vtoclg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtoclg.2	⊢ 𝜑

Assertion

Ref	Expression
vtoclg	⊢ (𝐴 ∈ 𝑉 → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		vtoclg.2	. . 3 ⊢ 𝜑
2		vtoclg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	mpbii 236	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4	3	vtocleg 3523	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840

This theorem is used by:  vtoclbg  3526  vtocl2g  3540  vtocl3g  3541  vtoclga  3543  nelrdva  3670  moeq3  3677  mo2icl  3679  sbcim1  3799  sbctt  3815  csbconstg  3873  sbcnestgfw  4386  sbcnestgf  4391  csbun  4406  csbin  4407  csbdif  4488  csbif  4547  axrep6g  5253  sepg  5261  inex1g  5290  ssexgOLD  5296  pwexg  5351  prexOLD  5416  sels  5423  opth  5460  csbopab  5542  csbopabw  5543  vtoclr  5726  resieq  5991  csbima12  6083  dmsnsnsn  6223  csbcog  6302  dfpred3g  6318  preddowncl  6337  ordelord  6386  iota5  6523  csbiota  6533  fconstg  6769  funbrfv  6933  fvelimab  6957  ssimaexg  6971  fvelrn  7075  isoselem  7348  csbriota  7391  csbov123  7463  ovg  7584  caovmo  7657  uniexg  7748  fnse  8135  onfununi  8334  rdg0g  8420  ensn1g  9025  fundmeng  9036  xpdom2g  9068  canth2g  9126  ssfi  9164  canthwdom  9548  zfregcl  9563  zfregclOLD  9564  elirr  9569  ttrclselem2  9702  tcvalg  9712  tz9.13g  9771  rankvalg  9796  ranklim  9823  r1pwALT  9825  rankuni2b  9832  rankuni  9842  cfslb2n  10267  itunitc1  10419  itunitc  10420  ituniiun  10421  hsmex  10431  axdc2lem  10447  ac7g  10473  ac6sg  10487  numthcor  10493  weth  10494  rankcf  10779  nqereu  10931  prnmax  10997  prlem936  11049  ltord1  11757  xmulasslem  13329  axdc4uz  14040  relexpind  15127  climshft  15653  telfsumo  15879  fsumparts  15883  lcmgcdlem  16688  mreacs  17738  dprdval  20121  fiinopn  23110  neiptoptop  23340  neiptopnei  23341  pt1hmeo  24016  isfildlem  24067  alexsublem  24254  ustuqtop4  24454  voliunlem3  25764  dvbsss  26114  dvfsumlem2  26239  acunirnmpt  33077  acunirnmpt2  33078  acunirnmpt2f  33079  carsgsigalem  34772  carsgclctunlem2  34776  carsgclctun  34778  pmeasmono  34781  pmeasadd  34782  sitgclg  34799  r1filimi  35557  mclsrcl  36092  iota5f  36255  shftvalg  36263  dfrdg2  36324  fvsingle  36449  fullfunfv  36478  ranksng  36698  rankelg  36699  rankpwg  36700  rankeq1o  36702  axtco1g  37046  csbttc  37079  ttcwf2  37095  ttcexg  37102  bj-adjg1  37738  mblfinlem3  38369  ismrer1  38549  mzpclall  43518  mzpcompact2  43543  diophrw  43550  monotuz  43728  monotoddzz  43730  oddcomabszz  43731  flcidc  43957  nzss  45087  pm14.122b  45193  sbiota1  45204  fiiuncl  45845  axccdom  45998  axccd  46004  monoords  46076  fperiodmullem  46082  0ellimcdiv  46423  cncfperiod  46653  icccncfext  46661  fperdvper  46693  dvnmul  46717  dvnprodlem2  46721  iblspltprt  46747  itgspltprt  46753  stoweidlem4  46778  stoweidlem6  46780  stoweidlem8  46782  stoweidlem15  46789  stoweidlem16  46790  stoweidlem19  46793  stoweidlem20  46794  stoweidlem22  46796  stoweidlem23  46797  stoweidlem27  46801  stoweidlem30  46804  stoweidlem32  46806  stoweidlem34  46808  stoweidlem42  46816  stoweidlem48  46822  fourierdlem11  46892  fourierdlem16  46897  fourierdlem21  46902  fourierdlem41  46922  fourierdlem42  46923  fourierdlem46  46926  fourierdlem48  46928  fourierdlem49  46929  fourierdlem50  46930  fourierdlem68  46948  fourierdlem72  46952  fourierdlem76  46956  fourierdlem79  46959  fourierdlem81  46961  fourierdlem89  46969  fourierdlem90  46970  fourierdlem91  46971  fourierdlem92  46972  fourierdlem97  46977  fourierdlem103  46983  fourierdlem104  46984  fourierdlem111  46991  sge0f1o  47156  sge0p1  47188  hoidmvlelem4  47372  smfpimcclem  47581  funressnmo  47843  aiota0def  47893  csbafv12g  47934  csbaovg  47977  csbafv212g  48016  funressndmafv2rn  48020  funressnbrafv2  48041  funbrafv2  48044