Theorem vtoclg 3518

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 3517	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-clel 2836

This theorem is used by:  vtoclbg  3520  vtocl2g  3534  vtocl3g  3535  vtoclga  3537  nelrdva  3663  moeq3  3670  mo2icl  3672  sbcim1  3792  sbctt  3808  csbconstg  3866  sbcnestgfw  4379  sbcnestgf  4384  csbun  4399  csbin  4400  csbdif  4481  csbif  4540  axrep6g  5243  sepg  5251  inex1g  5279  ssexgOLD  5285  pwexg  5340  prexOLD  5401  sels  5408  opth  5445  csbopab  5530  csbopabw  5531  vtoclr  5714  resieq  5981  csbima12  6076  dmsnsnsn  6221  csbcog  6300  dfpred3g  6316  preddowncl  6335  ordelord  6384  iota5  6521  csbiota  6531  fconstg  6769  funbrfv  6933  fvelimab  6957  ssimaexg  6971  fvelrn  7076  isoselem  7349  csbriota  7392  csbov123  7464  ovg  7585  caovmo  7658  uniexg  7757  fnse  8150  onfununi  8349  rdg0g  8435  ensn1g  9049  fundmeng  9060  xpdom2g  9092  canth2g  9150  ssfi  9188  canthwdom  9573  zfregcl  9588  zfregclOLD  9589  elirr  9594  ttrclselem2  9727  tcvalg  9737  tz9.13g  9799  rankvalg  9826  rankelg  9852  rankpwg  9857  ranklim  9858  r1pwALT  9860  rankuni2b  9867  ranksng  9874  rankuni  9879  r1filimi  9903  cfslb2n  10346  itunitc1  10498  itunitc  10499  ituniiun  10500  hsmex  10510  axdc2lem  10526  ac7g  10552  ac6sg  10566  numthcor  10572  weth  10573  rankcf  10862  nqereu  11014  prnmax  11080  prlem936  11132  ltord1  11842  xmulasslem  13415  axdc4uz  14127  relexpind  15217  climshft  15743  telfsumo  15969  fsumparts  15973  lcmgcdlem  16781  mreacs  17832  dprdval  20219  fiinopn  23219  neiptoptop  23449  neiptopnei  23450  pt1hmeo  24125  isfildlem  24176  alexsublem  24363  ustuqtop4  24563  voliunlem3  25873  dvbsss  26222  dvfsumlem2  26347  acunirnmpt  33253  acunirnmpt2  33254  acunirnmpt2f  33255  carsgsigalem  34947  carsgclctunlem2  34951  carsgclctun  34953  pmeasmono  34956  pmeasadd  34957  sitgclg  34974  mclsrcl  36326  iota5f  36489  shftvalg  36497  dfrdg2  36557  fvsingle  36682  fullfunfv  36711  rankeq1o  36932  axtco1g  37264  csbttc  37297  ttcwf2  37313  ttcexg  37320  bj-adjg1  37956  mblfinlem3  38577  ismrer1  38772  mzpclall  43737  mzpcompact2  43762  diophrw  43769  monotuz  43947  monotoddzz  43949  oddcomabszz  43950  flcidc  44171  nzss  45300  pm14.122b  45406  sbiota1  45417  fiiuncl  46081  axccdom  46234  axccd  46240  monoords  46312  fperiodmullem  46318  0ellimcdiv  46658  cncfperiod  46888  icccncfext  46896  fperdvper  46928  dvnmul  46952  dvnprodlem2  46956  iblspltprt  46982  itgspltprt  46988  stoweidlem4  47013  stoweidlem6  47015  stoweidlem8  47017  stoweidlem15  47024  stoweidlem16  47025  stoweidlem19  47028  stoweidlem20  47029  stoweidlem22  47031  stoweidlem23  47032  stoweidlem27  47036  stoweidlem30  47039  stoweidlem32  47041  stoweidlem34  47043  stoweidlem42  47051  stoweidlem48  47057  fourierdlem11  47127  fourierdlem16  47132  fourierdlem21  47137  fourierdlem41  47157  fourierdlem42  47158  fourierdlem46  47161  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem68  47183  fourierdlem72  47187  fourierdlem76  47191  fourierdlem79  47194  fourierdlem81  47196  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem92  47207  fourierdlem97  47212  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  sge0f1o  47391  sge0p1  47423  hoidmvlelem4  47607  smfpimcclem  47816  funressnmo  48115  aiota0def  48165  csbafv12g  48206  csbaovg  48249  csbafv212g  48288  funressndmafv2rn  48292  funressnbrafv2  48313  funbrafv2  48316