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  5316  prexOLD  5381  sels  5388  opth  5425  csbopab  5504  csbopabgALT  5505  vtoclr  5688  resieq  5950  csbima12  6039  dmsnsnsn  6179  csbcog  6256  dfpred3g  6272  preddowncl  6291  ordelord  6340  iota5  6476  csbiota  6486  fconstg  6722  funbrfv  6883  fvelimab  6907  ssimaexg  6921  fvelrn  7023  isoselem  7290  csbriota  7333  csbov123  7405  ovg  7526  caovmo  7598  uniexg  7688  fnse  8077  onfununi  8275  rdg0g  8360  ensn1g  8963  fundmeng  8973  xpdom2g  9005  canth2g  9063  ssfi  9101  canthwdom  9488  zfregcl  9503  zfregclOLD  9504  elirr  9508  ttrclselem2  9641  tcvalg  9651  tz9.13g  9710  rankvalg  9735  ranklim  9762  r1pwALT  9764  rankuni2b  9771  rankuni  9781  cfslb2n  10184  itunitc1  10336  itunitc  10337  ituniiun  10338  hsmex  10348  axdc2lem  10364  ac7g  10390  ac6sg  10404  numthcor  10410  weth  10411  rankcf  10694  nqereu  10846  prnmax  10912  prlem936  10964  ltord1  11670  xmulasslem  13231  axdc4uz  13940  relexpind  15020  climshft  15532  telfsumo  15759  fsumparts  15763  lcmgcdlem  16569  mreacs  17618  dprdval  19974  fiinopn  22879  neiptoptop  23109  neiptopnei  23110  pt1hmeo  23784  isfildlem  23835  alexsublem  24022  ustuqtop4  24222  voliunlem3  25532  dvbsss  25882  dvfsumlem2  26007  acunirnmpt  32750  acunirnmpt2  32751  acunirnmpt2f  32752  carsgsigalem  34478  carsgclctunlem2  34482  carsgclctun  34484  pmeasmono  34487  pmeasadd  34488  sitgclg  34505  r1filimi  35265  mclsrcl  35762  iota5f  35925  shftvalg  35933  dfrdg2  35994  fvsingle  36119  fullfunfv  36148  ranksng  36368  rankelg  36369  rankpwg  36370  rankeq1o  36372  axtco1g  36677  csbttc  36710  ttcwf2  36726  ttcexg  36733  bj-adjg1  37369  mblfinlem3  37997  ismrer1  38176  mzpclall  43176  mzpcompact2  43201  diophrw  43208  monotuz  43390  monotoddzz  43392  oddcomabszz  43393  flcidc  43619  nzss  44765  pm14.122b  44871  sbiota1  44882  fiiuncl  45517  axccdom  45672  axccd  45679  monoords  45751  fperiodmullem  45757  0ellimcdiv  46098  cncfperiod  46328  icccncfext  46336  fperdvper  46368  dvnmul  46392  dvnprodlem2  46396  iblspltprt  46422  itgspltprt  46428  stoweidlem4  46453  stoweidlem6  46455  stoweidlem8  46457  stoweidlem15  46464  stoweidlem16  46465  stoweidlem19  46468  stoweidlem20  46469  stoweidlem22  46471  stoweidlem23  46472  stoweidlem27  46476  stoweidlem30  46479  stoweidlem32  46481  stoweidlem34  46483  stoweidlem42  46491  stoweidlem48  46497  fourierdlem11  46567  fourierdlem16  46572  fourierdlem21  46577  fourierdlem41  46597  fourierdlem42  46598  fourierdlem46  46601  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem68  46623  fourierdlem72  46627  fourierdlem76  46631  fourierdlem79  46634  fourierdlem81  46636  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem92  46647  fourierdlem97  46652  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  sge0f1o  46831  sge0p1  46863  hoidmvlelem4  47047  smfpimcclem  47256  funressnmo  47509  aiota0def  47559  csbafv12g  47600  csbaovg  47643  csbafv212g  47682  funressndmafv2rn  47686  funressnbrafv2  47707  funbrafv2  47710