Theorem vtoclg 3534

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2167. (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 232	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4	3	vtocleg 3533	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-clel 2803

This theorem is referenced by:  vtoclbg  3537  vtocl2g  3555  vtocl3g  3556  vtoclga  3558  nelrdva  3699  moeq3  3706  mo2icl  3708  sbcim1  3833  sbctt  3852  csbconstg  3911  sbcnestgfw  4423  sbcnestgf  4428  csbun  4443  csbin  4444  csbdif  4532  csbif  4590  axrep6g  5298  inex1g  5324  ssexg  5328  pwexg  5382  prex  5438  sels  5444  opth  5482  csbopab  5561  csbopabgALT  5562  vtoclr  5745  resieq  6000  csbima12  6088  dmsnsnsn  6231  csbcog  6308  dfpred3g  6324  predbrg  6334  preddowncl  6345  ordelord  6398  iota5  6537  csbiota  6547  funmoOLD  6575  funimaexgOLD  6646  fconstg  6789  funbrfv  6952  fvelimab  6975  ssimaexg  6988  fvelrn  7090  isoselem  7353  csbriota  7396  csbov123  7467  ovg  7591  caovmo  7663  uniexg  7751  fnse  8147  onfununi  8371  rdg0g  8457  ensn1g  9055  fundmeng  9068  xpdom2g  9106  canth2g  9169  ssfi  9211  php2OLD  9257  canthwdom  9622  zfregcl  9637  elirr  9640  ttrclselem2  9769  tcvalg  9781  tz9.13g  9835  rankvalg  9860  ranklim  9887  r1pwALT  9889  rankuni2b  9896  rankuni  9906  cfslb2n  10311  itunitc1  10463  itunitc  10464  ituniiun  10465  hsmex  10475  axdc2lem  10491  ac7g  10517  ac6sg  10531  numthcor  10537  weth  10538  pwfseqlem4  10705  rankcf  10820  nqereu  10972  prnmax  11038  prlem936  11090  ltord1  11790  xmulasslem  13318  axdc4uz  14004  relexpind  15069  climshft  15578  telfsumo  15806  fsumparts  15810  lcmgcdlem  16607  mreacs  17671  dprdval  20003  fiinopn  22894  neiptoptop  23126  neiptopnei  23127  pt1hmeo  23801  isfildlem  23852  alexsublem  24039  ustuqtop4  24240  voliunlem3  25572  dvbsss  25922  dvfsumlem2  26052  dvfsumlem2OLD  26053  acunirnmpt  32576  acunirnmpt2  32577  acunirnmpt2f  32578  carsgsigalem  34149  carsgclctunlem2  34153  carsgclctun  34155  pmeasmono  34158  pmeasadd  34159  sitgclg  34176  mclsrcl  35389  iota5f  35546  shftvalg  35554  dfrdg2  35619  fvsingle  35744  fullfunfv  35771  ranksng  35991  rankelg  35992  rankpwg  35993  rankeq1o  35995  bj-adjg1  36750  mblfinlem3  37360  ismrer1  37539  mzpclall  42384  mzpcompact2  42409  diophrw  42416  monotuz  42599  monotoddzz  42601  oddcomabszz  42602  flcidc  42835  nzss  43991  pm14.122b  44097  sbiota1  44108  fiiuncl  44666  axccdom  44829  axccd  44836  monoords  44912  fperiodmullem  44918  0ellimcdiv  45270  cncfperiod  45500  icccncfext  45508  fperdvper  45540  dvnmul  45564  dvnprodlem2  45568  iblspltprt  45594  itgspltprt  45600  stoweidlem4  45625  stoweidlem6  45627  stoweidlem8  45629  stoweidlem15  45636  stoweidlem16  45637  stoweidlem19  45640  stoweidlem20  45641  stoweidlem22  45643  stoweidlem23  45644  stoweidlem27  45648  stoweidlem30  45651  stoweidlem32  45653  stoweidlem34  45655  stoweidlem42  45663  stoweidlem48  45669  fourierdlem11  45739  fourierdlem16  45744  fourierdlem21  45749  fourierdlem41  45769  fourierdlem42  45770  fourierdlem46  45773  fourierdlem48  45775  fourierdlem49  45776  fourierdlem50  45777  fourierdlem68  45795  fourierdlem72  45799  fourierdlem76  45803  fourierdlem79  45806  fourierdlem81  45808  fourierdlem89  45816  fourierdlem90  45817  fourierdlem91  45818  fourierdlem92  45819  fourierdlem97  45824  fourierdlem103  45830  fourierdlem104  45831  fourierdlem111  45838  sge0f1o  46003  sge0p1  46035  hoidmvlelem4  46219  smfpimcclem  46428  funressnmo  46661  aiota0def  46709  csbafv12g  46750  csbaovg  46793  csbafv212g  46832  funressndmafv2rn  46836  funressnbrafv2  46857  funbrafv2  46860