Theorem vtoclg 3538

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-clel 2810

This theorem is referenced by:  vtoclbg  3541  vtocl2g  3558  vtocl3g  3559  vtoclga  3561  nelrdva  3693  moeq3  3700  mo2icl  3702  sbcim1  3824  sbctt  3840  csbconstg  3898  sbcnestgfw  4401  sbcnestgf  4406  csbun  4421  csbin  4422  csbdif  4504  csbif  4563  axrep6g  5265  inex1g  5294  ssexg  5298  pwexg  5353  prex  5412  sels  5418  opth  5456  csbopab  5535  csbopabgALT  5536  vtoclr  5722  resieq  5982  csbima12  6071  dmsnsnsn  6214  csbcog  6291  dfpred3g  6307  preddowncl  6326  ordelord  6379  iota5  6519  csbiota  6529  funmoOLD  6557  funimaexgOLD  6629  fconstg  6770  funbrfv  6932  fvelimab  6956  ssimaexg  6970  fvelrn  7071  isoselem  7339  csbriota  7382  csbov123  7454  ovg  7577  caovmo  7649  uniexg  7739  fnse  8137  onfununi  8360  rdg0g  8446  ensn1g  9041  fundmeng  9051  xpdom2g  9087  canth2g  9150  ssfi  9192  php2OLD  9237  canthwdom  9598  zfregcl  9613  elirr  9616  ttrclselem2  9745  tcvalg  9757  tz9.13g  9811  rankvalg  9836  ranklim  9863  r1pwALT  9865  rankuni2b  9872  rankuni  9882  cfslb2n  10287  itunitc1  10439  itunitc  10440  ituniiun  10441  hsmex  10451  axdc2lem  10467  ac7g  10493  ac6sg  10507  numthcor  10513  weth  10514  rankcf  10796  nqereu  10948  prnmax  11014  prlem936  11066  ltord1  11768  xmulasslem  13306  axdc4uz  14007  relexpind  15088  climshft  15597  telfsumo  15823  fsumparts  15827  lcmgcdlem  16630  mreacs  17675  dprdval  19991  fiinopn  22844  neiptoptop  23074  neiptopnei  23075  pt1hmeo  23749  isfildlem  23800  alexsublem  23987  ustuqtop4  24188  voliunlem3  25510  dvbsss  25860  dvfsumlem2  25990  dvfsumlem2OLD  25991  acunirnmpt  32642  acunirnmpt2  32643  acunirnmpt2f  32644  carsgsigalem  34352  carsgclctunlem2  34356  carsgclctun  34358  pmeasmono  34361  pmeasadd  34362  sitgclg  34379  mclsrcl  35588  iota5f  35746  shftvalg  35754  dfrdg2  35818  fvsingle  35943  fullfunfv  35970  ranksng  36190  rankelg  36191  rankpwg  36192  rankeq1o  36194  bj-adjg1  37066  mblfinlem3  37688  ismrer1  37867  mzpclall  42725  mzpcompact2  42750  diophrw  42757  monotuz  42940  monotoddzz  42942  oddcomabszz  42943  flcidc  43169  nzss  44316  pm14.122b  44422  sbiota1  44433  fiiuncl  45069  axccdom  45226  axccd  45233  monoords  45306  fperiodmullem  45312  0ellimcdiv  45658  cncfperiod  45888  icccncfext  45896  fperdvper  45928  dvnmul  45952  dvnprodlem2  45956  iblspltprt  45982  itgspltprt  45988  stoweidlem4  46013  stoweidlem6  46015  stoweidlem8  46017  stoweidlem15  46024  stoweidlem16  46025  stoweidlem19  46028  stoweidlem20  46029  stoweidlem22  46031  stoweidlem23  46032  stoweidlem27  46036  stoweidlem30  46039  stoweidlem32  46041  stoweidlem34  46043  stoweidlem42  46051  stoweidlem48  46057  fourierdlem11  46127  fourierdlem16  46132  fourierdlem21  46137  fourierdlem41  46157  fourierdlem42  46158  fourierdlem46  46161  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem68  46183  fourierdlem72  46187  fourierdlem76  46191  fourierdlem79  46194  fourierdlem81  46196  fourierdlem89  46204  fourierdlem90  46205  fourierdlem91  46206  fourierdlem92  46207  fourierdlem97  46212  fourierdlem103  46218  fourierdlem104  46219  fourierdlem111  46226  sge0f1o  46391  sge0p1  46423  hoidmvlelem4  46607  smfpimcclem  46816  funressnmo  47055  aiota0def  47105  csbafv12g  47146  csbaovg  47189  csbafv212g  47228  funressndmafv2rn  47232  funressnbrafv2  47253  funbrafv2  47256