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  6763  funbrfv  6927  fvelimab  6951  ssimaexg  6965  fvelrn  7070  isoselem  7343  csbriota  7386  csbov123  7458  ovg  7579  caovmo  7652  uniexg  7743  fnse  8132  onfununi  8331  rdg0g  8417  ensn1g  9031  fundmeng  9042  xpdom2g  9074  canth2g  9132  ssfi  9170  canthwdom  9554  zfregcl  9569  zfregclOLD  9570  elirr  9575  ttrclselem2  9708  tcvalg  9718  tz9.13g  9777  rankvalg  9802  ranklim  9829  r1pwALT  9831  rankuni2b  9838  rankuni  9848  cfslb2n  10273  itunitc1  10425  itunitc  10426  ituniiun  10427  hsmex  10437  axdc2lem  10453  ac7g  10479  ac6sg  10493  numthcor  10499  weth  10500  rankcf  10789  nqereu  10941  prnmax  11007  prlem936  11059  ltord1  11767  xmulasslem  13340  axdc4uz  14051  relexpind  15140  climshft  15666  telfsumo  15892  fsumparts  15896  lcmgcdlem  16699  mreacs  17749  dprdval  20135  fiinopn  23129  neiptoptop  23359  neiptopnei  23360  pt1hmeo  24035  isfildlem  24086  alexsublem  24273  ustuqtop4  24473  voliunlem3  25783  dvbsss  26132  dvfsumlem2  26257  acunirnmpt  33135  acunirnmpt2  33136  acunirnmpt2f  33137  carsgsigalem  34829  carsgclctunlem2  34833  carsgclctun  34835  pmeasmono  34838  pmeasadd  34839  sitgclg  34856  r1filimi  35614  mclsrcl  36143  iota5f  36306  shftvalg  36314  dfrdg2  36375  fvsingle  36500  fullfunfv  36529  ranksng  36750  rankelg  36751  rankpwg  36752  rankeq1o  36754  axtco1g  37098  csbttc  37131  ttcwf2  37147  ttcexg  37154  bj-adjg1  37790  mblfinlem3  38411  ismrer1  38591  mzpclall  43575  mzpcompact2  43600  diophrw  43607  monotuz  43785  monotoddzz  43787  oddcomabszz  43788  flcidc  44014  nzss  45144  pm14.122b  45250  sbiota1  45261  fiiuncl  45902  axccdom  46055  axccd  46061  monoords  46133  fperiodmullem  46139  0ellimcdiv  46480  cncfperiod  46710  icccncfext  46718  fperdvper  46750  dvnmul  46774  dvnprodlem2  46778  iblspltprt  46804  itgspltprt  46810  stoweidlem4  46835  stoweidlem6  46837  stoweidlem8  46839  stoweidlem15  46846  stoweidlem16  46847  stoweidlem19  46850  stoweidlem20  46851  stoweidlem22  46853  stoweidlem23  46854  stoweidlem27  46858  stoweidlem30  46861  stoweidlem32  46863  stoweidlem34  46865  stoweidlem42  46873  stoweidlem48  46879  fourierdlem11  46949  fourierdlem16  46954  fourierdlem21  46959  fourierdlem41  46979  fourierdlem42  46980  fourierdlem46  46983  fourierdlem48  46985  fourierdlem49  46986  fourierdlem50  46987  fourierdlem68  47005  fourierdlem72  47009  fourierdlem76  47013  fourierdlem79  47016  fourierdlem81  47018  fourierdlem89  47026  fourierdlem90  47027  fourierdlem91  47028  fourierdlem92  47029  fourierdlem97  47034  fourierdlem103  47040  fourierdlem104  47041  fourierdlem111  47048  sge0f1o  47213  sge0p1  47245  hoidmvlelem4  47429  smfpimcclem  47638  funressnmo  47937  aiota0def  47987  csbafv12g  48028  csbaovg  48071  csbafv212g  48110  funressndmafv2rn  48114  funressnbrafv2  48135  funbrafv2  48138