Theorem vtoclg 3500

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-clel 2814

This theorem is referenced by:  vtoclbg  3502  vtocl2g  3517  vtocl3g  3518  vtoclga  3520  nelrdva  3646  moeq3  3653  mo2icl  3655  sbcim1  3776  sbctt  3792  csbconstg  3850  sbcnestgfw  4350  sbcnestgf  4355  csbun  4370  csbin  4371  csbdif  4454  csbif  4513  axrep6g  5213  inex1g  5248  ssexg  5252  pwexg  5308  prexOLD  5373  sels  5380  opth  5417  csbopab  5498  csbopabgALT  5499  vtoclr  5682  resieq  5943  csbima12  6032  dmsnsnsn  6172  csbcog  6249  dfpred3g  6265  preddowncl  6284  ordelord  6333  iota5  6469  csbiota  6479  fconstg  6715  funbrfv  6876  fvelimab  6900  ssimaexg  6914  fvelrn  7018  isoselem  7286  csbriota  7329  csbov123  7401  ovg  7522  caovmo  7594  uniexg  7684  fnse  8074  onfununi  8272  rdg0g  8357  ensn1g  8960  fundmeng  8970  xpdom2g  9002  canth2g  9060  ssfi  9098  canthwdom  9485  zfregcl  9500  zfregclOLD  9501  elirr  9506  ttrclselem2  9639  tcvalg  9649  tz9.13g  9708  rankvalg  9733  ranklim  9760  r1pwALT  9762  rankuni2b  9769  rankuni  9779  cfslb2n  10182  itunitc1  10334  itunitc  10335  ituniiun  10336  hsmex  10346  axdc2lem  10362  ac7g  10388  ac6sg  10402  numthcor  10408  weth  10409  rankcf  10692  nqereu  10844  prnmax  10910  prlem936  10962  ltord1  11668  xmulasslem  13229  axdc4uz  13938  relexpind  15018  climshft  15530  telfsumo  15757  fsumparts  15761  lcmgcdlem  16567  mreacs  17616  dprdval  19972  fiinopn  22885  neiptoptop  23115  neiptopnei  23116  pt1hmeo  23790  isfildlem  23841  alexsublem  24028  ustuqtop4  24228  voliunlem3  25538  dvbsss  25888  dvfsumlem2  26013  acunirnmpt  32752  acunirnmpt2  32753  acunirnmpt2f  32754  carsgsigalem  34508  carsgclctunlem2  34512  carsgclctun  34514  pmeasmono  34517  pmeasadd  34518  sitgclg  34535  r1filimi  35293  mclsrcl  35798  iota5f  35961  shftvalg  35969  dfrdg2  36030  fvsingle  36155  fullfunfv  36184  ranksng  36404  rankelg  36405  rankpwg  36406  rankeq1o  36408  axtco1g  36713  csbttc  36746  ttcwf2  36762  ttcexg  36769  bj-adjg1  37405  mblfinlem3  38035  ismrer1  38214  mzpclall  43185  mzpcompact2  43210  diophrw  43217  monotuz  43395  monotoddzz  43397  oddcomabszz  43398  flcidc  43624  nzss  44770  pm14.122b  44876  sbiota1  44887  fiiuncl  45522  axccdom  45675  axccd  45681  monoords  45753  fperiodmullem  45759  0ellimcdiv  46100  cncfperiod  46330  icccncfext  46338  fperdvper  46370  dvnmul  46394  dvnprodlem2  46398  iblspltprt  46424  itgspltprt  46430  stoweidlem4  46455  stoweidlem6  46457  stoweidlem8  46459  stoweidlem15  46466  stoweidlem16  46467  stoweidlem19  46470  stoweidlem20  46471  stoweidlem22  46473  stoweidlem23  46474  stoweidlem27  46478  stoweidlem30  46481  stoweidlem32  46483  stoweidlem34  46485  stoweidlem42  46493  stoweidlem48  46499  fourierdlem11  46569  fourierdlem16  46574  fourierdlem21  46579  fourierdlem41  46599  fourierdlem42  46600  fourierdlem46  46603  fourierdlem48  46605  fourierdlem49  46606  fourierdlem50  46607  fourierdlem68  46625  fourierdlem72  46629  fourierdlem76  46633  fourierdlem79  46636  fourierdlem81  46638  fourierdlem89  46646  fourierdlem90  46647  fourierdlem91  46648  fourierdlem92  46649  fourierdlem97  46654  fourierdlem103  46660  fourierdlem104  46661  fourierdlem111  46668  sge0f1o  46833  sge0p1  46865  hoidmvlelem4  47049  smfpimcclem  47258  funressnmo  47517  aiota0def  47567  csbafv12g  47608  csbaovg  47651  csbafv212g  47690  funressndmafv2rn  47694  funressnbrafv2  47715  funbrafv2  47718