Theorem vtoclg 3509

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-clel 2809

This theorem is referenced by:  vtoclbg  3512  vtocl2g  3527  vtocl3g  3528  vtoclga  3530  nelrdva  3661  moeq3  3668  mo2icl  3670  sbcim1  3792  sbctt  3808  csbconstg  3866  sbcnestgfw  4371  sbcnestgf  4376  csbun  4391  csbin  4392  csbdif  4476  csbif  4535  axrep6g  5233  inex1g  5262  ssexg  5266  pwexg  5321  prex  5380  sels  5386  opth  5422  csbopab  5501  csbopabgALT  5502  vtoclr  5685  resieq  5947  csbima12  6036  dmsnsnsn  6176  csbcog  6253  dfpred3g  6269  preddowncl  6288  ordelord  6337  iota5  6473  csbiota  6483  fconstg  6719  funbrfv  6880  fvelimab  6904  ssimaexg  6918  fvelrn  7019  isoselem  7285  csbriota  7328  csbov123  7400  ovg  7521  caovmo  7593  uniexg  7683  fnse  8073  onfununi  8271  rdg0g  8356  ensn1g  8957  fundmeng  8967  xpdom2g  8999  canth2g  9057  ssfi  9095  canthwdom  9482  zfregcl  9497  zfregclOLD  9498  elirr  9502  ttrclselem2  9633  tcvalg  9643  tz9.13g  9702  rankvalg  9727  ranklim  9754  r1pwALT  9756  rankuni2b  9763  rankuni  9773  cfslb2n  10176  itunitc1  10328  itunitc  10329  ituniiun  10330  hsmex  10340  axdc2lem  10356  ac7g  10382  ac6sg  10396  numthcor  10402  weth  10403  rankcf  10686  nqereu  10838  prnmax  10904  prlem936  10956  ltord1  11661  xmulasslem  13198  axdc4uz  13905  relexpind  14985  climshft  15497  telfsumo  15723  fsumparts  15727  lcmgcdlem  16531  mreacs  17579  dprdval  19932  fiinopn  22843  neiptoptop  23073  neiptopnei  23074  pt1hmeo  23748  isfildlem  23799  alexsublem  23986  ustuqtop4  24186  voliunlem3  25507  dvbsss  25857  dvfsumlem2  25987  dvfsumlem2OLD  25988  acunirnmpt  32686  acunirnmpt2  32687  acunirnmpt2f  32688  carsgsigalem  34421  carsgclctunlem2  34425  carsgclctun  34427  pmeasmono  34430  pmeasadd  34431  sitgclg  34448  r1filimi  35208  mclsrcl  35704  iota5f  35867  shftvalg  35875  dfrdg2  35936  fvsingle  36061  fullfunfv  36090  ranksng  36310  rankelg  36311  rankpwg  36312  rankeq1o  36314  bj-adjg1  37187  mblfinlem3  37799  ismrer1  37978  mzpclall  42911  mzpcompact2  42936  diophrw  42943  monotuz  43125  monotoddzz  43127  oddcomabszz  43128  flcidc  43354  nzss  44500  pm14.122b  44606  sbiota1  44617  fiiuncl  45252  axccdom  45408  axccd  45415  monoords  45487  fperiodmullem  45493  0ellimcdiv  45835  cncfperiod  46065  icccncfext  46073  fperdvper  46105  dvnmul  46129  dvnprodlem2  46133  iblspltprt  46159  itgspltprt  46165  stoweidlem4  46190  stoweidlem6  46192  stoweidlem8  46194  stoweidlem15  46201  stoweidlem16  46202  stoweidlem19  46205  stoweidlem20  46206  stoweidlem22  46208  stoweidlem23  46209  stoweidlem27  46213  stoweidlem30  46216  stoweidlem32  46218  stoweidlem34  46220  stoweidlem42  46228  stoweidlem48  46234  fourierdlem11  46304  fourierdlem16  46309  fourierdlem21  46314  fourierdlem41  46334  fourierdlem42  46335  fourierdlem46  46338  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem68  46360  fourierdlem72  46364  fourierdlem76  46368  fourierdlem79  46371  fourierdlem81  46373  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem92  46384  fourierdlem97  46389  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  sge0f1o  46568  sge0p1  46600  hoidmvlelem4  46784  smfpimcclem  46993  funressnmo  47234  aiota0def  47284  csbafv12g  47325  csbaovg  47368  csbafv212g  47407  funressndmafv2rn  47411  funressnbrafv2  47432  funbrafv2  47435