Theorem vtoclg 3511

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

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

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 2115

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

This theorem is referenced by:  vtoclbg  3514  vtocl2g  3529  vtocl3g  3530  vtoclga  3532  nelrdva  3663  moeq3  3670  mo2icl  3672  sbcim1  3794  sbctt  3810  csbconstg  3868  sbcnestgfw  4373  sbcnestgf  4378  csbun  4393  csbin  4394  csbdif  4478  csbif  4537  axrep6g  5235  inex1g  5264  ssexg  5268  pwexg  5323  prex  5382  sels  5388  opth  5424  csbopab  5503  csbopabgALT  5504  vtoclr  5687  resieq  5949  csbima12  6038  dmsnsnsn  6178  csbcog  6255  dfpred3g  6271  preddowncl  6290  ordelord  6339  iota5  6475  csbiota  6485  fconstg  6721  funbrfv  6882  fvelimab  6906  ssimaexg  6920  fvelrn  7021  isoselem  7287  csbriota  7330  csbov123  7402  ovg  7523  caovmo  7595  uniexg  7685  fnse  8075  onfununi  8273  rdg0g  8358  ensn1g  8961  fundmeng  8971  xpdom2g  9003  canth2g  9061  ssfi  9099  canthwdom  9486  zfregcl  9501  zfregclOLD  9502  elirr  9506  ttrclselem2  9637  tcvalg  9647  tz9.13g  9706  rankvalg  9731  ranklim  9758  r1pwALT  9760  rankuni2b  9767  rankuni  9777  cfslb2n  10180  itunitc1  10332  itunitc  10333  ituniiun  10334  hsmex  10344  axdc2lem  10360  ac7g  10386  ac6sg  10400  numthcor  10406  weth  10407  rankcf  10690  nqereu  10842  prnmax  10908  prlem936  10960  ltord1  11665  xmulasslem  13202  axdc4uz  13909  relexpind  14989  climshft  15501  telfsumo  15727  fsumparts  15731  lcmgcdlem  16535  mreacs  17583  dprdval  19936  fiinopn  22847  neiptoptop  23077  neiptopnei  23078  pt1hmeo  23752  isfildlem  23803  alexsublem  23990  ustuqtop4  24190  voliunlem3  25511  dvbsss  25861  dvfsumlem2  25991  dvfsumlem2OLD  25992  acunirnmpt  32739  acunirnmpt2  32740  acunirnmpt2f  32741  carsgsigalem  34474  carsgclctunlem2  34478  carsgclctun  34480  pmeasmono  34483  pmeasadd  34484  sitgclg  34501  r1filimi  35261  mclsrcl  35757  iota5f  35920  shftvalg  35928  dfrdg2  35989  fvsingle  36114  fullfunfv  36143  ranksng  36363  rankelg  36364  rankpwg  36365  rankeq1o  36367  bj-adjg1  37246  mblfinlem3  37862  ismrer1  38041  mzpclall  42990  mzpcompact2  43015  diophrw  43022  monotuz  43204  monotoddzz  43206  oddcomabszz  43207  flcidc  43433  nzss  44579  pm14.122b  44685  sbiota1  44696  fiiuncl  45331  axccdom  45487  axccd  45494  monoords  45566  fperiodmullem  45572  0ellimcdiv  45914  cncfperiod  46144  icccncfext  46152  fperdvper  46184  dvnmul  46208  dvnprodlem2  46212  iblspltprt  46238  itgspltprt  46244  stoweidlem4  46269  stoweidlem6  46271  stoweidlem8  46273  stoweidlem15  46280  stoweidlem16  46281  stoweidlem19  46284  stoweidlem20  46285  stoweidlem22  46287  stoweidlem23  46288  stoweidlem27  46292  stoweidlem30  46295  stoweidlem32  46297  stoweidlem34  46299  stoweidlem42  46307  stoweidlem48  46313  fourierdlem11  46383  fourierdlem16  46388  fourierdlem21  46393  fourierdlem41  46413  fourierdlem42  46414  fourierdlem46  46417  fourierdlem48  46419  fourierdlem49  46420  fourierdlem50  46421  fourierdlem68  46439  fourierdlem72  46443  fourierdlem76  46447  fourierdlem79  46450  fourierdlem81  46452  fourierdlem89  46460  fourierdlem90  46461  fourierdlem91  46462  fourierdlem92  46463  fourierdlem97  46468  fourierdlem103  46474  fourierdlem104  46475  fourierdlem111  46482  sge0f1o  46647  sge0p1  46679  hoidmvlelem4  46863  smfpimcclem  47072  funressnmo  47313  aiota0def  47363  csbafv12g  47404  csbaovg  47447  csbafv212g  47486  funressndmafv2rn  47490  funressnbrafv2  47511  funbrafv2  47514