Theorem vtoclg 3499

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-clel 2811

This theorem is referenced by:  vtoclbg  3502  vtocl2g  3517  vtocl3g  3518  vtoclga  3520  nelrdva  3651  moeq3  3658  mo2icl  3660  sbcim1  3782  sbctt  3798  csbconstg  3856  sbcnestgfw  4361  sbcnestgf  4366  csbun  4381  csbin  4382  csbdif  4465  csbif  4524  axrep6g  5225  inex1g  5260  ssexg  5264  pwexg  5320  prexOLD  5385  sels  5392  opth  5429  csbopab  5510  csbopabgALT  5511  vtoclr  5694  resieq  5955  csbima12  6044  dmsnsnsn  6184  csbcog  6261  dfpred3g  6277  preddowncl  6296  ordelord  6345  iota5  6481  csbiota  6491  fconstg  6727  funbrfv  6888  fvelimab  6912  ssimaexg  6926  fvelrn  7028  isoselem  7296  csbriota  7339  csbov123  7411  ovg  7532  caovmo  7604  uniexg  7694  fnse  8083  onfununi  8281  rdg0g  8366  ensn1g  8969  fundmeng  8979  xpdom2g  9011  canth2g  9069  ssfi  9107  canthwdom  9494  zfregcl  9509  zfregclOLD  9510  elirr  9514  ttrclselem2  9647  tcvalg  9657  tz9.13g  9716  rankvalg  9741  ranklim  9768  r1pwALT  9770  rankuni2b  9777  rankuni  9787  cfslb2n  10190  itunitc1  10342  itunitc  10343  ituniiun  10344  hsmex  10354  axdc2lem  10370  ac7g  10396  ac6sg  10410  numthcor  10416  weth  10417  rankcf  10700  nqereu  10852  prnmax  10918  prlem936  10970  ltord1  11676  xmulasslem  13237  axdc4uz  13946  relexpind  15026  climshft  15538  telfsumo  15765  fsumparts  15769  lcmgcdlem  16575  mreacs  17624  dprdval  19980  fiinopn  22866  neiptoptop  23096  neiptopnei  23097  pt1hmeo  23771  isfildlem  23822  alexsublem  24009  ustuqtop4  24209  voliunlem3  25519  dvbsss  25869  dvfsumlem2  25994  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  carsgsigalem  34459  carsgclctunlem2  34463  carsgclctun  34465  pmeasmono  34468  pmeasadd  34469  sitgclg  34486  r1filimi  35246  mclsrcl  35743  iota5f  35906  shftvalg  35914  dfrdg2  35975  fvsingle  36100  fullfunfv  36129  ranksng  36349  rankelg  36350  rankpwg  36351  rankeq1o  36353  axtco1g  36658  csbttc  36691  ttcwf2  36707  ttcexg  36714  bj-adjg1  37350  mblfinlem3  37980  ismrer1  38159  mzpclall  43159  mzpcompact2  43184  diophrw  43191  monotuz  43369  monotoddzz  43371  oddcomabszz  43372  flcidc  43598  nzss  44744  pm14.122b  44850  sbiota1  44861  fiiuncl  45496  axccdom  45651  axccd  45658  monoords  45730  fperiodmullem  45736  0ellimcdiv  46077  cncfperiod  46307  icccncfext  46315  fperdvper  46347  dvnmul  46371  dvnprodlem2  46375  iblspltprt  46401  itgspltprt  46407  stoweidlem4  46432  stoweidlem6  46434  stoweidlem8  46436  stoweidlem15  46443  stoweidlem16  46444  stoweidlem19  46447  stoweidlem20  46448  stoweidlem22  46450  stoweidlem23  46451  stoweidlem27  46455  stoweidlem30  46458  stoweidlem32  46460  stoweidlem34  46462  stoweidlem42  46470  stoweidlem48  46476  fourierdlem11  46546  fourierdlem16  46551  fourierdlem21  46556  fourierdlem41  46576  fourierdlem42  46577  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem68  46602  fourierdlem72  46606  fourierdlem76  46610  fourierdlem79  46613  fourierdlem81  46615  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  sge0f1o  46810  sge0p1  46842  hoidmvlelem4  47026  smfpimcclem  47235  funressnmo  47494  aiota0def  47544  csbafv12g  47585  csbaovg  47628  csbafv212g  47667  funressndmafv2rn  47671  funressnbrafv2  47692  funbrafv2  47695