Theorem vtoclg 3523

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 235	. 2 ⊢ (𝑥 = 𝐴 → 𝜓)
4	3	vtocleg 3522	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-clel 2838

This theorem is referenced by:  vtoclbg  3525  vtocl2g  3539  vtocl3g  3540  vtoclga  3542  nelrdva  3669  moeq3  3676  mo2icl  3678  sbcim1  3798  sbctt  3814  csbconstg  3872  sbcnestgfw  4376  sbcnestgf  4381  csbun  4396  csbin  4397  csbdif  4480  csbif  4539  axrep6g  5241  inex1g  5276  ssexg  5280  pwexg  5336  prexOLD  5401  sels  5408  opth  5445  csbopab  5527  csbopabw  5528  vtoclr  5711  resieq  5977  csbima12  6069  dmsnsnsn  6208  csbcog  6285  dfpred3g  6301  preddowncl  6320  ordelord  6369  iota5  6505  csbiota  6515  fconstg  6752  funbrfv  6916  fvelimab  6940  ssimaexg  6954  fvelrn  7058  isoselem  7326  csbriota  7369  csbov123  7441  ovg  7562  caovmo  7634  uniexg  7724  fnse  8114  onfununi  8313  rdg0g  8399  ensn1g  9004  fundmeng  9014  xpdom2g  9046  canth2g  9104  ssfi  9142  canthwdom  9528  zfregcl  9543  zfregclOLD  9544  elirr  9549  ttrclselem2  9682  tcvalg  9692  tz9.13g  9751  rankvalg  9776  ranklim  9803  r1pwALT  9805  rankuni2b  9812  rankuni  9822  cfslb2n  10226  itunitc1  10378  itunitc  10379  ituniiun  10380  hsmex  10390  axdc2lem  10406  ac7g  10432  ac6sg  10446  numthcor  10452  weth  10453  rankcf  10736  nqereu  10888  prnmax  10954  prlem936  11006  ltord1  11714  xmulasslem  13289  axdc4uz  13998  relexpind  15078  climshft  15604  telfsumo  15831  fsumparts  15835  lcmgcdlem  16641  mreacs  17691  dprdval  20046  fiinopn  22962  neiptoptop  23192  neiptopnei  23193  pt1hmeo  23867  isfildlem  23918  alexsublem  24105  ustuqtop4  24305  voliunlem3  25615  dvbsss  25965  dvfsumlem2  26090  acunirnmpt  32862  acunirnmpt2  32863  acunirnmpt2f  32864  carsgsigalem  34613  carsgclctunlem2  34617  carsgclctun  34619  pmeasmono  34622  pmeasadd  34623  sitgclg  34640  r1filimi  35400  mclsrcl  35912  iota5f  36075  shftvalg  36083  dfrdg2  36144  fvsingle  36269  fullfunfv  36298  ranksng  36518  rankelg  36519  rankpwg  36520  rankeq1o  36522  axtco1g  36837  csbttc  36870  ttcwf2  36886  ttcexg  36893  bj-adjg1  37529  mblfinlem3  38159  ismrer1  38338  mzpclall  43309  mzpcompact2  43334  diophrw  43341  monotuz  43519  monotoddzz  43521  oddcomabszz  43522  flcidc  43748  nzss  44894  pm14.122b  45000  sbiota1  45011  fiiuncl  45646  axccdom  45799  axccd  45805  monoords  45877  fperiodmullem  45883  0ellimcdiv  46224  cncfperiod  46454  icccncfext  46462  fperdvper  46494  dvnmul  46518  dvnprodlem2  46522  iblspltprt  46548  itgspltprt  46554  stoweidlem4  46579  stoweidlem6  46581  stoweidlem8  46583  stoweidlem15  46590  stoweidlem16  46591  stoweidlem19  46594  stoweidlem20  46595  stoweidlem22  46597  stoweidlem23  46598  stoweidlem27  46602  stoweidlem30  46605  stoweidlem32  46607  stoweidlem34  46609  stoweidlem42  46617  stoweidlem48  46623  fourierdlem11  46693  fourierdlem16  46698  fourierdlem21  46703  fourierdlem41  46723  fourierdlem42  46724  fourierdlem46  46727  fourierdlem48  46729  fourierdlem49  46730  fourierdlem50  46731  fourierdlem68  46749  fourierdlem72  46753  fourierdlem76  46757  fourierdlem79  46760  fourierdlem81  46762  fourierdlem89  46770  fourierdlem90  46771  fourierdlem91  46772  fourierdlem92  46773  fourierdlem97  46778  fourierdlem103  46784  fourierdlem104  46785  fourierdlem111  46792  sge0f1o  46957  sge0p1  46989  hoidmvlelem4  47173  smfpimcclem  47382  funressnmo  47641  aiota0def  47691  csbafv12g  47732  csbaovg  47775  csbafv212g  47814  funressndmafv2rn  47818  funressnbrafv2  47839  funbrafv2  47842