Theorem vtoclg 3557

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-clel 2811

This theorem is referenced by:  vtoclbg  3560  vtocl2g  3563  vtocl3g  3564  vtoclga  3566  nelrdva  3702  moeq3  3709  mo2icl  3711  sbcim1  3834  sbctt  3854  csbconstg  3913  sbcnestgfw  4419  sbcnestgf  4424  csbun  4439  csbin  4440  csbdif  4528  csbif  4586  axrep6g  5294  inex1g  5320  ssexg  5324  pwexg  5377  prex  5433  sels  5439  opth  5477  csbopab  5556  csbopabgALT  5557  vtoclr  5740  resieq  5993  csbima12  6079  dmsnsnsn  6220  csbcog  6297  dfpred3g  6313  predbrg  6323  preddowncl  6334  ordelord  6387  iota5  6527  csbiota  6537  funmoOLD  6565  funimaexgOLD  6636  fconstg  6779  funbrfv  6943  fvelimab  6965  ssimaexg  6978  fvelrn  7079  isoselem  7338  csbriota  7381  csbov123  7451  ovg  7572  caovmo  7644  uniexg  7730  fnse  8119  onfununi  8341  rdg0g  8427  ensn1g  9019  fundmeng  9032  xpdom2g  9068  canth2g  9131  ssfi  9173  php2OLD  9223  canthwdom  9574  zfregcl  9589  elirr  9592  ttrclselem2  9721  tcvalg  9733  tz9.13g  9787  rankvalg  9812  ranklim  9839  r1pwALT  9841  rankuni2b  9848  rankuni  9858  cfslb2n  10263  itunitc1  10415  itunitc  10416  ituniiun  10417  hsmex  10427  axdc2lem  10443  ac7g  10469  ac6sg  10483  numthcor  10489  weth  10490  pwfseqlem4  10657  rankcf  10772  nqereu  10924  prnmax  10990  prlem936  11042  ltord1  11740  xmulasslem  13264  axdc4uz  13949  relexpind  15011  climshft  15520  telfsumo  15748  fsumparts  15752  lcmgcdlem  16543  mreacs  17602  dprdval  19873  fiinopn  22403  neiptoptop  22635  neiptopnei  22636  pt1hmeo  23310  isfildlem  23361  alexsublem  23548  ustuqtop4  23749  voliunlem3  25069  dvbsss  25419  dvfsumlem2  25544  acunirnmpt  31915  acunirnmpt2  31916  acunirnmpt2f  31917  carsgsigalem  33345  carsgclctunlem2  33349  carsgclctun  33351  pmeasmono  33354  pmeasadd  33355  sitgclg  33372  mclsrcl  34583  iota5f  34724  shftvalg  34732  dfrdg2  34798  fvsingle  34923  fullfunfv  34950  ranksng  35170  rankelg  35171  rankpwg  35172  rankeq1o  35174  gg-dvfsumlem2  35214  bj-adjg1  35972  mblfinlem3  36575  ismrer1  36754  mzpclall  41513  mzpcompact2  41538  diophrw  41545  monotuz  41728  monotoddzz  41730  oddcomabszz  41731  flcidc  41964  nzss  43124  pm14.122b  43230  sbiota1  43241  fiiuncl  43800  axccdom  43969  axccd  43976  monoords  44055  fperiodmullem  44061  0ellimcdiv  44413  cncfperiod  44643  icccncfext  44651  fperdvper  44683  dvnmul  44707  dvnprodlem2  44711  iblspltprt  44737  itgspltprt  44743  stoweidlem4  44768  stoweidlem6  44770  stoweidlem8  44772  stoweidlem15  44779  stoweidlem16  44780  stoweidlem19  44783  stoweidlem20  44784  stoweidlem22  44786  stoweidlem23  44787  stoweidlem27  44791  stoweidlem30  44794  stoweidlem32  44796  stoweidlem34  44798  stoweidlem42  44806  stoweidlem48  44812  fourierdlem11  44882  fourierdlem16  44887  fourierdlem21  44892  fourierdlem41  44912  fourierdlem42  44913  fourierdlem46  44916  fourierdlem48  44918  fourierdlem49  44919  fourierdlem50  44920  fourierdlem68  44938  fourierdlem72  44942  fourierdlem76  44946  fourierdlem79  44949  fourierdlem81  44951  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem92  44962  fourierdlem97  44967  fourierdlem103  44973  fourierdlem104  44974  fourierdlem111  44981  sge0f1o  45146  sge0p1  45178  hoidmvlelem4  45362  smfpimcclem  45571  funressnmo  45804  aiota0def  45852  csbafv12g  45893  csbaovg  45936  csbafv212g  45975  funressndmafv2rn  45979  funressnbrafv2  46000  funbrafv2  46003