Theorem vtoclg 3531

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2219. (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 3530	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-clel 2844

This theorem is referenced by:  vtoclbg  3533  vtocl2g  3547  vtocl3g  3548  vtoclga  3550  nelrdva  3677  moeq3  3684  mo2icl  3686  sbcim1  3806  sbctt  3822  csbconstg  3880  sbcnestgfw  4392  sbcnestgf  4397  csbun  4412  csbin  4413  csbdif  4491  csbif  4550  axrep6g  5255  inex1g  5290  ssexg  5294  pwexg  5350  prexOLD  5415  sels  5422  opth  5459  csbopab  5541  csbopabw  5542  vtoclr  5725  resieq  5990  csbima12  6082  dmsnsnsn  6222  csbcog  6299  dfpred3g  6315  preddowncl  6334  ordelord  6383  iota5  6520  csbiota  6530  fconstg  6766  funbrfv  6930  fvelimab  6954  ssimaexg  6968  fvelrn  7072  isoselem  7340  csbriota  7383  csbov123  7455  ovg  7576  caovmo  7648  uniexg  7739  fnse  8129  onfununi  8328  rdg0g  8414  ensn1g  9019  fundmeng  9029  xpdom2g  9061  canth2g  9119  ssfi  9157  canthwdom  9541  zfregcl  9556  zfregclOLD  9557  elirr  9562  ttrclselem2  9695  tcvalg  9705  tz9.13g  9764  rankvalg  9789  ranklim  9816  r1pwALT  9818  rankuni2b  9825  rankuni  9835  cfslb2n  10252  itunitc1  10404  itunitc  10405  ituniiun  10406  hsmex  10416  axdc2lem  10432  ac7g  10458  ac6sg  10472  numthcor  10478  weth  10479  rankcf  10762  nqereu  10914  prnmax  10980  prlem936  11032  ltord1  11740  xmulasslem  13311  axdc4uz  14020  relexpind  15101  climshft  15627  telfsumo  15854  fsumparts  15858  lcmgcdlem  16664  mreacs  17714  dprdval  20075  fiinopn  23027  neiptoptop  23257  neiptopnei  23258  pt1hmeo  23932  isfildlem  23983  alexsublem  24170  ustuqtop4  24370  voliunlem3  25680  dvbsss  26030  dvfsumlem2  26155  acunirnmpt  32945  acunirnmpt2  32946  acunirnmpt2f  32947  carsgsigalem  34650  carsgclctunlem2  34654  carsgclctun  34656  pmeasmono  34659  pmeasadd  34660  sitgclg  34677  r1filimi  35440  mclsrcl  35986  iota5f  36149  shftvalg  36157  dfrdg2  36218  fvsingle  36343  fullfunfv  36372  ranksng  36592  rankelg  36593  rankpwg  36594  rankeq1o  36596  axtco1g  36910  csbttc  36943  ttcwf2  36959  ttcexg  36966  bj-adjg1  37601  mblfinlem3  38232  ismrer1  38411  mzpclall  43384  mzpcompact2  43409  diophrw  43416  monotuz  43594  monotoddzz  43596  oddcomabszz  43597  flcidc  43823  nzss  44953  pm14.122b  45059  sbiota1  45070  fiiuncl  45711  axccdom  45864  axccd  45870  monoords  45942  fperiodmullem  45948  0ellimcdiv  46289  cncfperiod  46519  icccncfext  46527  fperdvper  46559  dvnmul  46583  dvnprodlem2  46587  iblspltprt  46613  itgspltprt  46619  stoweidlem4  46644  stoweidlem6  46646  stoweidlem8  46648  stoweidlem15  46655  stoweidlem16  46656  stoweidlem19  46659  stoweidlem20  46660  stoweidlem22  46662  stoweidlem23  46663  stoweidlem27  46667  stoweidlem30  46670  stoweidlem32  46672  stoweidlem34  46674  stoweidlem42  46682  stoweidlem48  46688  fourierdlem11  46758  fourierdlem16  46763  fourierdlem21  46768  fourierdlem41  46788  fourierdlem42  46789  fourierdlem46  46792  fourierdlem48  46794  fourierdlem49  46795  fourierdlem50  46796  fourierdlem68  46814  fourierdlem72  46818  fourierdlem76  46822  fourierdlem79  46825  fourierdlem81  46827  fourierdlem89  46835  fourierdlem90  46836  fourierdlem91  46837  fourierdlem92  46838  fourierdlem97  46843  fourierdlem103  46849  fourierdlem104  46850  fourierdlem111  46857  sge0f1o  47022  sge0p1  47054  hoidmvlelem4  47238  smfpimcclem  47447  funressnmo  47706  aiota0def  47756  csbafv12g  47797  csbaovg  47840  csbafv212g  47879  funressndmafv2rn  47883  funressnbrafv2  47904  funbrafv2  47907