Theorem vtoclg 3507

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2180. (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 3506	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  vtoclbg  3510  vtocl2g  3525  vtocl3g  3526  vtoclga  3528  nelrdva  3659  moeq3  3666  mo2icl  3668  sbcim1  3790  sbctt  3806  csbconstg  3864  sbcnestgfw  4368  sbcnestgf  4373  csbun  4388  csbin  4389  csbdif  4471  csbif  4530  axrep6g  5226  inex1g  5255  ssexg  5259  pwexg  5314  prex  5373  sels  5379  opth  5414  csbopab  5493  csbopabgALT  5494  vtoclr  5677  resieq  5938  csbima12  6027  dmsnsnsn  6167  csbcog  6244  dfpred3g  6260  preddowncl  6279  ordelord  6328  iota5  6464  csbiota  6474  fconstg  6710  funbrfv  6870  fvelimab  6894  ssimaexg  6908  fvelrn  7009  isoselem  7275  csbriota  7318  csbov123  7390  ovg  7511  caovmo  7583  uniexg  7673  fnse  8063  onfununi  8261  rdg0g  8346  ensn1g  8944  fundmeng  8954  xpdom2g  8986  canth2g  9044  ssfi  9082  canthwdom  9465  zfregcl  9480  zfregclOLD  9481  elirr  9485  ttrclselem2  9616  tcvalg  9626  tz9.13g  9685  rankvalg  9710  ranklim  9737  r1pwALT  9739  rankuni2b  9746  rankuni  9756  cfslb2n  10159  itunitc1  10311  itunitc  10312  ituniiun  10313  hsmex  10323  axdc2lem  10339  ac7g  10365  ac6sg  10379  numthcor  10385  weth  10386  rankcf  10668  nqereu  10820  prnmax  10886  prlem936  10938  ltord1  11643  xmulasslem  13184  axdc4uz  13891  relexpind  14971  climshft  15483  telfsumo  15709  fsumparts  15713  lcmgcdlem  16517  mreacs  17564  dprdval  19917  fiinopn  22816  neiptoptop  23046  neiptopnei  23047  pt1hmeo  23721  isfildlem  23772  alexsublem  23959  ustuqtop4  24159  voliunlem3  25480  dvbsss  25830  dvfsumlem2  25960  dvfsumlem2OLD  25961  acunirnmpt  32641  acunirnmpt2  32642  acunirnmpt2f  32643  carsgsigalem  34328  carsgclctunlem2  34332  carsgclctun  34334  pmeasmono  34337  pmeasadd  34338  sitgclg  34355  r1filimi  35114  mclsrcl  35605  iota5f  35768  shftvalg  35776  dfrdg2  35837  fvsingle  35962  fullfunfv  35991  ranksng  36211  rankelg  36212  rankpwg  36213  rankeq1o  36215  bj-adjg1  37087  mblfinlem3  37709  ismrer1  37888  mzpclall  42830  mzpcompact2  42855  diophrw  42862  monotuz  43044  monotoddzz  43046  oddcomabszz  43047  flcidc  43273  nzss  44420  pm14.122b  44526  sbiota1  44537  fiiuncl  45172  axccdom  45329  axccd  45336  monoords  45408  fperiodmullem  45414  0ellimcdiv  45757  cncfperiod  45987  icccncfext  45995  fperdvper  46027  dvnmul  46051  dvnprodlem2  46055  iblspltprt  46081  itgspltprt  46087  stoweidlem4  46112  stoweidlem6  46114  stoweidlem8  46116  stoweidlem15  46123  stoweidlem16  46124  stoweidlem19  46127  stoweidlem20  46128  stoweidlem22  46130  stoweidlem23  46131  stoweidlem27  46135  stoweidlem30  46138  stoweidlem32  46140  stoweidlem34  46142  stoweidlem42  46150  stoweidlem48  46156  fourierdlem11  46226  fourierdlem16  46231  fourierdlem21  46236  fourierdlem41  46256  fourierdlem42  46257  fourierdlem46  46260  fourierdlem48  46262  fourierdlem49  46263  fourierdlem50  46264  fourierdlem68  46282  fourierdlem72  46286  fourierdlem76  46290  fourierdlem79  46293  fourierdlem81  46295  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem92  46306  fourierdlem97  46311  fourierdlem103  46317  fourierdlem104  46318  fourierdlem111  46325  sge0f1o  46490  sge0p1  46522  hoidmvlelem4  46706  smfpimcclem  46915  funressnmo  47156  aiota0def  47206  csbafv12g  47247  csbaovg  47290  csbafv212g  47329  funressndmafv2rn  47333  funressnbrafv2  47354  funbrafv2  47357