Theorem vtoclg 3517

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 3516	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 2739  df-clel 2835

This theorem is used by:  vtoclbg  3519  vtocl2g  3533  vtocl3g  3534  vtoclga  3536  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  5245  sepg  5253  inex1g  5282  ssexgOLD  5288  pwexg  5343  prexOLD  5408  sels  5415  opth  5452  csbopab  5534  csbopabw  5535  vtoclr  5718  resieq  5983  csbima12  6075  dmsnsnsn  6216  csbcog  6295  dfpred3g  6311  preddowncl  6330  ordelord  6379  iota5  6516  csbiota  6526  fconstg  6762  funbrfv  6926  fvelimab  6950  ssimaexg  6964  fvelrn  7069  isoselem  7342  csbriota  7385  csbov123  7457  ovg  7578  caovmo  7651  uniexg  7742  fnse  8131  onfununi  8330  rdg0g  8416  ensn1g  9028  fundmeng  9039  xpdom2g  9071  canth2g  9129  ssfi  9167  canthwdom  9551  zfregcl  9566  zfregclOLD  9567  elirr  9572  ttrclselem2  9705  tcvalg  9715  tz9.13g  9774  rankvalg  9799  ranklim  9826  r1pwALT  9828  rankuni2b  9835  rankuni  9845  cfslb2n  10270  itunitc1  10422  itunitc  10423  ituniiun  10424  hsmex  10434  axdc2lem  10450  ac7g  10476  ac6sg  10490  numthcor  10496  weth  10497  rankcf  10786  nqereu  10938  prnmax  11004  prlem936  11056  ltord1  11764  xmulasslem  13337  axdc4uz  14048  relexpind  15137  climshft  15663  telfsumo  15889  fsumparts  15893  lcmgcdlem  16696  mreacs  17746  dprdval  20132  fiinopn  23126  neiptoptop  23356  neiptopnei  23357  pt1hmeo  24032  isfildlem  24083  alexsublem  24270  ustuqtop4  24470  voliunlem3  25780  dvbsss  26129  dvfsumlem2  26254  acunirnmpt  33132  acunirnmpt2  33133  acunirnmpt2f  33134  carsgsigalem  34826  carsgclctunlem2  34830  carsgclctun  34832  pmeasmono  34835  pmeasadd  34836  sitgclg  34853  r1filimi  35611  mclsrcl  36140  iota5f  36303  shftvalg  36311  dfrdg2  36372  fvsingle  36497  fullfunfv  36526  ranksng  36747  rankelg  36748  rankpwg  36749  rankeq1o  36751  axtco1g  37095  csbttc  37128  ttcwf2  37144  ttcexg  37151  bj-adjg1  37787  mblfinlem3  38408  ismrer1  38588  mzpclall  43572  mzpcompact2  43597  diophrw  43604  monotuz  43782  monotoddzz  43784  oddcomabszz  43785  flcidc  44011  nzss  45141  pm14.122b  45247  sbiota1  45258  fiiuncl  45899  axccdom  46052  axccd  46058  monoords  46130  fperiodmullem  46136  0ellimcdiv  46477  cncfperiod  46707  icccncfext  46715  fperdvper  46747  dvnmul  46771  dvnprodlem2  46775  iblspltprt  46801  itgspltprt  46807  stoweidlem4  46832  stoweidlem6  46834  stoweidlem8  46836  stoweidlem15  46843  stoweidlem16  46844  stoweidlem19  46847  stoweidlem20  46848  stoweidlem22  46850  stoweidlem23  46851  stoweidlem27  46855  stoweidlem30  46858  stoweidlem32  46860  stoweidlem34  46862  stoweidlem42  46870  stoweidlem48  46876  fourierdlem11  46946  fourierdlem16  46951  fourierdlem21  46956  fourierdlem41  46976  fourierdlem42  46977  fourierdlem46  46980  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem68  47002  fourierdlem72  47006  fourierdlem76  47010  fourierdlem79  47013  fourierdlem81  47015  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem92  47026  fourierdlem97  47031  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  sge0f1o  47210  sge0p1  47242  hoidmvlelem4  47426  smfpimcclem  47635  funressnmo  47934  aiota0def  47984  csbafv12g  48025  csbaovg  48068  csbafv212g  48107  funressndmafv2rn  48111  funressnbrafv2  48132  funbrafv2  48135