Theorem vtoclg 3522

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-clel 2838

This theorem is referenced by:  vtoclbg  3524  vtocl2g  3538  vtocl3g  3539  vtoclga  3541  nelrdva  3668  moeq3  3675  mo2icl  3677  sbcim1  3797  sbctt  3813  csbconstg  3872  sbcnestgfw  4386  sbcnestgf  4391  csbun  4406  csbin  4407  csbdif  4486  csbif  4545  axrep6g  5251  sepg  5259  inex1g  5288  ssexgOLD  5294  pwexg  5349  prexOLD  5414  sels  5421  opth  5458  csbopab  5540  csbopabw  5541  vtoclr  5724  resieq  5989  csbima12  6081  dmsnsnsn  6221  csbcog  6298  dfpred3g  6314  preddowncl  6333  ordelord  6382  iota5  6519  csbiota  6529  fconstg  6765  funbrfv  6929  fvelimab  6953  ssimaexg  6967  fvelrn  7071  isoselem  7339  csbriota  7382  csbov123  7454  ovg  7575  caovmo  7647  uniexg  7738  fnse  8125  onfununi  8324  rdg0g  8410  ensn1g  9015  fundmeng  9025  xpdom2g  9057  canth2g  9115  ssfi  9153  canthwdom  9537  zfregcl  9552  zfregclOLD  9553  elirr  9558  ttrclselem2  9691  tcvalg  9701  tz9.13g  9760  rankvalg  9785  ranklim  9812  r1pwALT  9814  rankuni2b  9821  rankuni  9831  cfslb2n  10247  itunitc1  10399  itunitc  10400  ituniiun  10401  hsmex  10411  axdc2lem  10427  ac7g  10453  ac6sg  10467  numthcor  10473  weth  10474  rankcf  10757  nqereu  10909  prnmax  10975  prlem936  11027  ltord1  11735  xmulasslem  13306  axdc4uz  14016  relexpind  15097  climshft  15623  telfsumo  15850  fsumparts  15854  lcmgcdlem  16659  mreacs  17709  dprdval  20070  fiinopn  23058  neiptoptop  23288  neiptopnei  23289  pt1hmeo  23963  isfildlem  24014  alexsublem  24201  ustuqtop4  24401  voliunlem3  25711  dvbsss  26061  dvfsumlem2  26186  acunirnmpt  33004  acunirnmpt2  33005  acunirnmpt2f  33006  carsgsigalem  34705  carsgclctunlem2  34709  carsgclctun  34711  pmeasmono  34714  pmeasadd  34715  sitgclg  34732  r1filimi  35497  mclsrcl  36053  iota5f  36216  shftvalg  36224  dfrdg2  36285  fvsingle  36410  fullfunfv  36439  ranksng  36659  rankelg  36660  rankpwg  36661  rankeq1o  36663  axtco1g  37007  csbttc  37040  ttcwf2  37056  ttcexg  37063  bj-adjg1  37699  mblfinlem3  38330  ismrer1  38509  mzpclall  43478  mzpcompact2  43503  diophrw  43510  monotuz  43688  monotoddzz  43690  oddcomabszz  43691  flcidc  43917  nzss  45047  pm14.122b  45153  sbiota1  45164  fiiuncl  45805  axccdom  45958  axccd  45964  monoords  46036  fperiodmullem  46042  0ellimcdiv  46383  cncfperiod  46613  icccncfext  46621  fperdvper  46653  dvnmul  46677  dvnprodlem2  46681  iblspltprt  46707  itgspltprt  46713  stoweidlem4  46738  stoweidlem6  46740  stoweidlem8  46742  stoweidlem15  46749  stoweidlem16  46750  stoweidlem19  46753  stoweidlem20  46754  stoweidlem22  46756  stoweidlem23  46757  stoweidlem27  46761  stoweidlem30  46764  stoweidlem32  46766  stoweidlem34  46768  stoweidlem42  46776  stoweidlem48  46782  fourierdlem11  46852  fourierdlem16  46857  fourierdlem21  46862  fourierdlem41  46882  fourierdlem42  46883  fourierdlem46  46886  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem68  46908  fourierdlem72  46912  fourierdlem76  46916  fourierdlem79  46919  fourierdlem81  46921  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  fourierdlem92  46932  fourierdlem97  46937  fourierdlem103  46943  fourierdlem104  46944  fourierdlem111  46951  sge0f1o  47116  sge0p1  47148  hoidmvlelem4  47332  smfpimcclem  47541  funressnmo  47803  aiota0def  47853  csbafv12g  47894  csbaovg  47937  csbafv212g  47976  funressndmafv2rn  47980  funressnbrafv2  48001  funbrafv2  48004