Theorem vtoclg 3500

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2185. (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 233	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4	3	vtocleg 3499	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  vtoclbg  3503  vtocl2g  3518  vtocl3g  3519  vtoclga  3521  nelrdva  3652  moeq3  3659  mo2icl  3661  sbcim1  3783  sbctt  3799  csbconstg  3857  sbcnestgfw  4362  sbcnestgf  4367  csbun  4382  csbin  4383  csbdif  4466  csbif  4525  axrep6g  5226  inex1g  5257  ssexg  5261  pwexg  5317  prexOLD  5382  sels  5389  opth  5426  csbopab  5505  csbopabgALT  5506  vtoclr  5689  resieq  5951  csbima12  6040  dmsnsnsn  6180  csbcog  6257  dfpred3g  6273  preddowncl  6292  ordelord  6341  iota5  6477  csbiota  6487  fconstg  6723  funbrfv  6884  fvelimab  6908  ssimaexg  6922  fvelrn  7024  isoselem  7291  csbriota  7334  csbov123  7406  ovg  7527  caovmo  7599  uniexg  7689  fnse  8078  onfununi  8276  rdg0g  8361  ensn1g  8964  fundmeng  8974  xpdom2g  9006  canth2g  9064  ssfi  9102  canthwdom  9489  zfregcl  9504  zfregclOLD  9505  elirr  9509  ttrclselem2  9642  tcvalg  9652  tz9.13g  9711  rankvalg  9736  ranklim  9763  r1pwALT  9765  rankuni2b  9772  rankuni  9782  cfslb2n  10185  itunitc1  10337  itunitc  10338  ituniiun  10339  hsmex  10349  axdc2lem  10365  ac7g  10391  ac6sg  10405  numthcor  10411  weth  10412  rankcf  10695  nqereu  10847  prnmax  10913  prlem936  10965  ltord1  11671  xmulasslem  13232  axdc4uz  13941  relexpind  15021  climshft  15533  telfsumo  15760  fsumparts  15764  lcmgcdlem  16570  mreacs  17619  dprdval  19975  fiinopn  22880  neiptoptop  23110  neiptopnei  23111  pt1hmeo  23785  isfildlem  23836  alexsublem  24023  ustuqtop4  24223  voliunlem3  25533  dvbsss  25883  dvfsumlem2  26008  acunirnmpt  32751  acunirnmpt2  32752  acunirnmpt2f  32753  carsgsigalem  34479  carsgclctunlem2  34483  carsgclctun  34485  pmeasmono  34488  pmeasadd  34489  sitgclg  34506  r1filimi  35266  mclsrcl  35763  iota5f  35926  shftvalg  35934  dfrdg2  35995  fvsingle  36120  fullfunfv  36149  ranksng  36369  rankelg  36370  rankpwg  36371  rankeq1o  36373  axtco1g  36678  csbttc  36711  ttcwf2  36727  ttcexg  36734  bj-adjg1  37370  mblfinlem3  37998  ismrer1  38177  mzpclall  43177  mzpcompact2  43202  diophrw  43209  monotuz  43391  monotoddzz  43393  oddcomabszz  43394  flcidc  43620  nzss  44766  pm14.122b  44872  sbiota1  44883  fiiuncl  45518  axccdom  45673  axccd  45680  monoords  45752  fperiodmullem  45758  0ellimcdiv  46099  cncfperiod  46329  icccncfext  46337  fperdvper  46369  dvnmul  46393  dvnprodlem2  46397  iblspltprt  46423  itgspltprt  46429  stoweidlem4  46454  stoweidlem6  46456  stoweidlem8  46458  stoweidlem15  46465  stoweidlem16  46466  stoweidlem19  46469  stoweidlem20  46470  stoweidlem22  46472  stoweidlem23  46473  stoweidlem27  46477  stoweidlem30  46480  stoweidlem32  46482  stoweidlem34  46484  stoweidlem42  46492  stoweidlem48  46498  fourierdlem11  46568  fourierdlem16  46573  fourierdlem21  46578  fourierdlem41  46598  fourierdlem42  46599  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem68  46624  fourierdlem72  46628  fourierdlem76  46632  fourierdlem79  46635  fourierdlem81  46637  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  sge0f1o  46832  sge0p1  46864  hoidmvlelem4  47048  smfpimcclem  47257  funressnmo  47510  aiota0def  47560  csbafv12g  47601  csbaovg  47644  csbafv212g  47683  funressndmafv2rn  47687  funressnbrafv2  47708  funbrafv2  47711