Theorem vtoclg 3513

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 3512	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 2716  df-clel 2812

This theorem is referenced by:  vtoclbg  3516  vtocl2g  3531  vtocl3g  3532  vtoclga  3534  nelrdva  3665  moeq3  3672  mo2icl  3674  sbcim1  3796  sbctt  3812  csbconstg  3870  sbcnestgfw  4375  sbcnestgf  4380  csbun  4395  csbin  4396  csbdif  4480  csbif  4539  axrep6g  5237  inex1g  5266  ssexg  5270  pwexg  5325  prexOLD  5389  sels  5395  opth  5432  csbopab  5511  csbopabgALT  5512  vtoclr  5695  resieq  5957  csbima12  6046  dmsnsnsn  6186  csbcog  6263  dfpred3g  6279  preddowncl  6298  ordelord  6347  iota5  6483  csbiota  6493  fconstg  6729  funbrfv  6890  fvelimab  6914  ssimaexg  6928  fvelrn  7030  isoselem  7297  csbriota  7340  csbov123  7412  ovg  7533  caovmo  7605  uniexg  7695  fnse  8085  onfununi  8283  rdg0g  8368  ensn1g  8971  fundmeng  8981  xpdom2g  9013  canth2g  9071  ssfi  9109  canthwdom  9496  zfregcl  9511  zfregclOLD  9512  elirr  9516  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  11675  xmulasslem  13212  axdc4uz  13919  relexpind  14999  climshft  15511  telfsumo  15737  fsumparts  15741  lcmgcdlem  16545  mreacs  17593  dprdval  19949  fiinopn  22860  neiptoptop  23090  neiptopnei  23091  pt1hmeo  23765  isfildlem  23816  alexsublem  24003  ustuqtop4  24203  voliunlem3  25524  dvbsss  25874  dvfsumlem2  26004  dvfsumlem2OLD  26005  acunirnmpt  32753  acunirnmpt2  32754  acunirnmpt2f  32755  carsgsigalem  34497  carsgclctunlem2  34501  carsgclctun  34503  pmeasmono  34506  pmeasadd  34507  sitgclg  34524  r1filimi  35284  mclsrcl  35781  iota5f  35944  shftvalg  35952  dfrdg2  36013  fvsingle  36138  fullfunfv  36167  ranksng  36387  rankelg  36388  rankpwg  36389  rankeq1o  36391  bj-adjg1  37295  mblfinlem3  37914  ismrer1  38093  mzpclall  43088  mzpcompact2  43113  diophrw  43120  monotuz  43302  monotoddzz  43304  oddcomabszz  43305  flcidc  43531  nzss  44677  pm14.122b  44783  sbiota1  44794  fiiuncl  45429  axccdom  45584  axccd  45591  monoords  45663  fperiodmullem  45669  0ellimcdiv  46011  cncfperiod  46241  icccncfext  46249  fperdvper  46281  dvnmul  46305  dvnprodlem2  46309  iblspltprt  46335  itgspltprt  46341  stoweidlem4  46366  stoweidlem6  46368  stoweidlem8  46370  stoweidlem15  46377  stoweidlem16  46378  stoweidlem19  46381  stoweidlem20  46382  stoweidlem22  46384  stoweidlem23  46385  stoweidlem27  46389  stoweidlem30  46392  stoweidlem32  46394  stoweidlem34  46396  stoweidlem42  46404  stoweidlem48  46410  fourierdlem11  46480  fourierdlem16  46485  fourierdlem21  46490  fourierdlem41  46510  fourierdlem42  46511  fourierdlem46  46514  fourierdlem48  46516  fourierdlem49  46517  fourierdlem50  46518  fourierdlem68  46536  fourierdlem72  46540  fourierdlem76  46544  fourierdlem79  46547  fourierdlem81  46549  fourierdlem89  46557  fourierdlem90  46558  fourierdlem91  46559  fourierdlem92  46560  fourierdlem97  46565  fourierdlem103  46571  fourierdlem104  46572  fourierdlem111  46579  sge0f1o  46744  sge0p1  46776  hoidmvlelem4  46960  smfpimcclem  47169  funressnmo  47410  aiota0def  47460  csbafv12g  47501  csbaovg  47544  csbafv212g  47583  funressndmafv2rn  47587  funressnbrafv2  47608  funbrafv2  47611