Theorem vtoclg 3521

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-clel 2839

This theorem is used by:  vtoclbg  3523  vtocl2g  3537  vtocl3g  3538  vtoclga  3540  nelrdva  3666  moeq3  3673  mo2icl  3675  sbcim1  3795  sbctt  3811  csbconstg  3870  sbcnestgfw  4382  sbcnestgf  4387  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  axrep6g  5246  sepg  5254  inex1g  5283  ssexgOLD  5289  pwexg  5344  prexOLD  5405  sels  5412  opth  5449  csbopab  5534  csbopabw  5535  vtoclr  5718  resieq  5986  csbima12  6082  dmsnsnsn  6228  csbcog  6307  dfpred3g  6323  preddowncl  6342  ordelord  6391  iota5  6529  csbiota  6540  fconstg  6780  funbrfv  6944  fvelimab  6968  ssimaexg  6982  fvelrn  7087  isoselem  7359  csbriota  7402  csbov123  7474  ovg  7595  caovmo  7668  uniexg  7767  fnse  8163  onfununi  8363  rdg0g  8449  ensn1g  9063  fundmeng  9074  xpdom2g  9106  canth2g  9164  ssfi  9202  canthwdom  9586  zfregcl  9601  zfregclOLD  9602  elirr  9607  ttrclselem2  9740  tcvalg  9750  tz9.13g  9812  rankvalg  9839  rankelg  9865  rankpwg  9870  ranklim  9871  r1pwALT  9873  rankuni2b  9880  ranksng  9887  rankuni  9892  r1filimi  9916  cfslb2n  10359  itunitc1  10511  itunitc  10512  ituniiun  10513  hsmex  10523  axdc2lem  10539  ac7g  10565  ac6sg  10579  numthcor  10585  weth  10586  rankcf  10875  nqereu  11027  prnmax  11093  prlem936  11145  ltord1  11855  xmulasslem  13428  axdc4uz  14140  relexpind  15232  climshft  15758  telfsumo  15984  fsumparts  15988  lcmgcdlem  16796  mreacs  17847  dprdval  20234  fiinopn  23234  neiptoptop  23464  neiptopnei  23465  pt1hmeo  24140  isfildlem  24191  alexsublem  24378  ustuqtop4  24578  voliunlem3  25888  dvbsss  26237  dvfsumlem2  26362  acunirnmpt  33310  carsgsigalem  35003  carsgclctunlem2  35007  carsgclctun  35009  pmeasmono  35012  pmeasadd  35013  sitgclg  35030  mclsrcl  36450  iota5f  36619  shftvalg  36627  dfrdg2  36687  fvsingle  36812  fullfunfv  36841  rankeq1o  37062  axtco1g  37394  csbttc  37427  ttcwf2  37443  ttcexg  37450  bj-adjg1  38086  mblfinlem3  38720  ismrer1  38915  mzpclall  43881  mzpcompact2  43906  diophrw  43913  monotuz  44091  monotoddzz  44093  oddcomabszz  44094  flcidc  44315  nzss  45444  pm14.122b  45549  sbiota1  45560  fiiuncl  46224  axccdom  46377  axccd  46383  monoords  46455  fperiodmullem  46461  0ellimcdiv  46801  cncfperiod  47031  icccncfext  47039  fperdvper  47071  dvnmul  47095  dvnprodlem2  47099  iblspltprt  47125  itgspltprt  47131  stoweidlem4  47156  stoweidlem6  47158  stoweidlem8  47160  stoweidlem15  47167  stoweidlem16  47168  stoweidlem19  47171  stoweidlem20  47172  stoweidlem22  47174  stoweidlem23  47175  stoweidlem27  47179  stoweidlem30  47182  stoweidlem32  47184  stoweidlem34  47186  stoweidlem42  47194  stoweidlem48  47200  fourierdlem11  47270  fourierdlem16  47275  fourierdlem21  47280  fourierdlem41  47300  fourierdlem42  47301  fourierdlem46  47304  fourierdlem48  47306  fourierdlem49  47307  fourierdlem50  47308  fourierdlem68  47326  fourierdlem72  47330  fourierdlem76  47334  fourierdlem79  47337  fourierdlem81  47339  fourierdlem89  47347  fourierdlem90  47348  fourierdlem91  47349  fourierdlem92  47350  fourierdlem97  47355  fourierdlem103  47361  fourierdlem104  47362  fourierdlem111  47369  sge0f1o  47534  sge0p1  47566  hoidmvlelem4  47750  smfpimcclem  47959  funressnmo  48258  aiota0def  48308  csbafv12g  48349  csbaovg  48392  csbafv212g  48431  funressndmafv2rn  48435  funressnbrafv2  48456  funbrafv2  48459