Theorem vtoclg 3520

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 3519	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 2708  df-clel 2803

This theorem is referenced by:  vtoclbg  3523  vtocl2g  3540  vtocl3g  3541  vtoclga  3543  nelrdva  3676  moeq3  3683  mo2icl  3685  sbcim1  3807  sbctt  3823  csbconstg  3881  sbcnestgfw  4384  sbcnestgf  4389  csbun  4404  csbin  4405  csbdif  4487  csbif  4546  axrep6g  5245  inex1g  5274  ssexg  5278  pwexg  5333  prex  5392  sels  5398  opth  5436  csbopab  5515  csbopabgALT  5516  vtoclr  5701  resieq  5961  csbima12  6050  dmsnsnsn  6193  csbcog  6270  dfpred3g  6286  preddowncl  6305  ordelord  6354  iota5  6494  csbiota  6504  funmoOLD  6532  funimaexgOLD  6604  fconstg  6747  funbrfv  6909  fvelimab  6933  ssimaexg  6947  fvelrn  7048  isoselem  7316  csbriota  7359  csbov123  7431  ovg  7554  caovmo  7626  uniexg  7716  fnse  8112  onfununi  8310  rdg0g  8395  ensn1g  8993  fundmeng  9003  xpdom2g  9037  canth2g  9095  ssfi  9137  canthwdom  9532  zfregcl  9547  elirr  9550  ttrclselem2  9679  tcvalg  9691  tz9.13g  9745  rankvalg  9770  ranklim  9797  r1pwALT  9799  rankuni2b  9806  rankuni  9816  cfslb2n  10221  itunitc1  10373  itunitc  10374  ituniiun  10375  hsmex  10385  axdc2lem  10401  ac7g  10427  ac6sg  10441  numthcor  10447  weth  10448  rankcf  10730  nqereu  10882  prnmax  10948  prlem936  11000  ltord1  11704  xmulasslem  13245  axdc4uz  13949  relexpind  15030  climshft  15542  telfsumo  15768  fsumparts  15772  lcmgcdlem  16576  mreacs  17619  dprdval  19935  fiinopn  22788  neiptoptop  23018  neiptopnei  23019  pt1hmeo  23693  isfildlem  23744  alexsublem  23931  ustuqtop4  24132  voliunlem3  25453  dvbsss  25803  dvfsumlem2  25933  dvfsumlem2OLD  25934  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  carsgsigalem  34306  carsgclctunlem2  34310  carsgclctun  34312  pmeasmono  34315  pmeasadd  34316  sitgclg  34333  mclsrcl  35548  iota5f  35711  shftvalg  35719  dfrdg2  35783  fvsingle  35908  fullfunfv  35935  ranksng  36155  rankelg  36156  rankpwg  36157  rankeq1o  36159  bj-adjg1  37031  mblfinlem3  37653  ismrer1  37832  mzpclall  42715  mzpcompact2  42740  diophrw  42747  monotuz  42930  monotoddzz  42932  oddcomabszz  42933  flcidc  43159  nzss  44306  pm14.122b  44412  sbiota1  44423  fiiuncl  45059  axccdom  45216  axccd  45223  monoords  45295  fperiodmullem  45301  0ellimcdiv  45647  cncfperiod  45877  icccncfext  45885  fperdvper  45917  dvnmul  45941  dvnprodlem2  45945  iblspltprt  45971  itgspltprt  45977  stoweidlem4  46002  stoweidlem6  46004  stoweidlem8  46006  stoweidlem15  46013  stoweidlem16  46014  stoweidlem19  46017  stoweidlem20  46018  stoweidlem22  46020  stoweidlem23  46021  stoweidlem27  46025  stoweidlem30  46028  stoweidlem32  46030  stoweidlem34  46032  stoweidlem42  46040  stoweidlem48  46046  fourierdlem11  46116  fourierdlem16  46121  fourierdlem21  46126  fourierdlem41  46146  fourierdlem42  46147  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem68  46172  fourierdlem72  46176  fourierdlem76  46180  fourierdlem79  46183  fourierdlem81  46185  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  sge0f1o  46380  sge0p1  46412  hoidmvlelem4  46596  smfpimcclem  46805  funressnmo  47047  aiota0def  47097  csbafv12g  47138  csbaovg  47181  csbafv212g  47220  funressndmafv2rn  47224  funressnbrafv2  47245  funbrafv2  47248