Theorem vtoclg 3517

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  vtoclbg  3520  vtocl2g  3537  vtocl3g  3538  vtoclga  3540  nelrdva  3673  moeq3  3680  mo2icl  3682  sbcim1  3804  sbctt  3820  csbconstg  3878  sbcnestgfw  4380  sbcnestgf  4385  csbun  4400  csbin  4401  csbdif  4483  csbif  4542  axrep6g  5240  inex1g  5269  ssexg  5273  pwexg  5328  prex  5387  sels  5393  opth  5431  csbopab  5510  csbopabgALT  5511  vtoclr  5694  resieq  5950  csbima12  6039  dmsnsnsn  6181  csbcog  6258  dfpred3g  6274  preddowncl  6293  ordelord  6342  iota5  6482  csbiota  6492  fconstg  6729  funbrfv  6891  fvelimab  6915  ssimaexg  6929  fvelrn  7030  isoselem  7298  csbriota  7341  csbov123  7413  ovg  7534  caovmo  7606  uniexg  7696  fnse  8089  onfununi  8287  rdg0g  8372  ensn1g  8970  fundmeng  8980  xpdom2g  9014  canth2g  9072  ssfi  9114  canthwdom  9508  zfregcl  9523  elirr  9526  ttrclselem2  9655  tcvalg  9667  tz9.13g  9721  rankvalg  9746  ranklim  9773  r1pwALT  9775  rankuni2b  9782  rankuni  9792  cfslb2n  10197  itunitc1  10349  itunitc  10350  ituniiun  10351  hsmex  10361  axdc2lem  10377  ac7g  10403  ac6sg  10417  numthcor  10423  weth  10424  rankcf  10706  nqereu  10858  prnmax  10924  prlem936  10976  ltord1  11680  xmulasslem  13221  axdc4uz  13925  relexpind  15006  climshft  15518  telfsumo  15744  fsumparts  15748  lcmgcdlem  16552  mreacs  17599  dprdval  19919  fiinopn  22821  neiptoptop  23051  neiptopnei  23052  pt1hmeo  23726  isfildlem  23777  alexsublem  23964  ustuqtop4  24165  voliunlem3  25486  dvbsss  25836  dvfsumlem2  25966  dvfsumlem2OLD  25967  acunirnmpt  32633  acunirnmpt2  32634  acunirnmpt2f  32635  carsgsigalem  34299  carsgclctunlem2  34303  carsgclctun  34305  pmeasmono  34308  pmeasadd  34309  sitgclg  34326  mclsrcl  35541  iota5f  35704  shftvalg  35712  dfrdg2  35776  fvsingle  35901  fullfunfv  35928  ranksng  36148  rankelg  36149  rankpwg  36150  rankeq1o  36152  bj-adjg1  37024  mblfinlem3  37646  ismrer1  37825  mzpclall  42708  mzpcompact2  42733  diophrw  42740  monotuz  42923  monotoddzz  42925  oddcomabszz  42926  flcidc  43152  nzss  44299  pm14.122b  44405  sbiota1  44416  fiiuncl  45052  axccdom  45209  axccd  45216  monoords  45288  fperiodmullem  45294  0ellimcdiv  45640  cncfperiod  45870  icccncfext  45878  fperdvper  45910  dvnmul  45934  dvnprodlem2  45938  iblspltprt  45964  itgspltprt  45970  stoweidlem4  45995  stoweidlem6  45997  stoweidlem8  45999  stoweidlem15  46006  stoweidlem16  46007  stoweidlem19  46010  stoweidlem20  46011  stoweidlem22  46013  stoweidlem23  46014  stoweidlem27  46018  stoweidlem30  46021  stoweidlem32  46023  stoweidlem34  46025  stoweidlem42  46033  stoweidlem48  46039  fourierdlem11  46109  fourierdlem16  46114  fourierdlem21  46119  fourierdlem41  46139  fourierdlem42  46140  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem68  46165  fourierdlem72  46169  fourierdlem76  46173  fourierdlem79  46176  fourierdlem81  46178  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem92  46189  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  sge0f1o  46373  sge0p1  46405  hoidmvlelem4  46589  smfpimcclem  46798  funressnmo  47040  aiota0def  47090  csbafv12g  47131  csbaovg  47174  csbafv212g  47213  funressndmafv2rn  47217  funressnbrafv2  47238  funbrafv2  47241