Theorem vtoclg 3553

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-clel 2813

This theorem is referenced by:  vtoclbg  3556  vtocl2g  3573  vtocl3g  3574  vtoclga  3576  nelrdva  3713  moeq3  3720  mo2icl  3722  sbcim1  3847  sbctt  3866  csbconstg  3926  sbcnestgfw  4426  sbcnestgf  4431  csbun  4446  csbin  4447  csbdif  4529  csbif  4587  axrep6g  5295  inex1g  5324  ssexg  5328  pwexg  5383  prex  5442  sels  5448  opth  5486  csbopab  5564  csbopabgALT  5565  vtoclr  5751  resieq  6010  csbima12  6098  dmsnsnsn  6241  csbcog  6318  dfpred3g  6334  preddowncl  6354  ordelord  6407  iota5  6545  csbiota  6555  funmoOLD  6583  funimaexgOLD  6654  fconstg  6795  funbrfv  6957  fvelimab  6980  ssimaexg  6994  fvelrn  7095  isoselem  7360  csbriota  7402  csbov123  7474  ovg  7597  caovmo  7669  uniexg  7758  fnse  8156  onfununi  8379  rdg0g  8465  ensn1g  9060  fundmeng  9070  xpdom2g  9106  canth2g  9169  ssfi  9211  php2OLD  9257  canthwdom  9616  zfregcl  9631  elirr  9634  ttrclselem2  9763  tcvalg  9775  tz9.13g  9829  rankvalg  9854  ranklim  9881  r1pwALT  9883  rankuni2b  9890  rankuni  9900  cfslb2n  10305  itunitc1  10457  itunitc  10458  ituniiun  10459  hsmex  10469  axdc2lem  10485  ac7g  10511  ac6sg  10525  numthcor  10531  weth  10532  rankcf  10814  nqereu  10966  prnmax  11032  prlem936  11084  ltord1  11786  xmulasslem  13323  axdc4uz  14021  relexpind  15099  climshft  15608  telfsumo  15834  fsumparts  15838  lcmgcdlem  16639  mreacs  17702  dprdval  20037  fiinopn  22922  neiptoptop  23154  neiptopnei  23155  pt1hmeo  23829  isfildlem  23880  alexsublem  24067  ustuqtop4  24268  voliunlem3  25600  dvbsss  25951  dvfsumlem2  26081  dvfsumlem2OLD  26082  acunirnmpt  32675  acunirnmpt2  32676  acunirnmpt2f  32677  carsgsigalem  34296  carsgclctunlem2  34300  carsgclctun  34302  pmeasmono  34305  pmeasadd  34306  sitgclg  34323  mclsrcl  35545  iota5f  35703  shftvalg  35711  dfrdg2  35776  fvsingle  35901  fullfunfv  35928  ranksng  36148  rankelg  36149  rankpwg  36150  rankeq1o  36152  bj-adjg1  37025  mblfinlem3  37645  ismrer1  37824  mzpclall  42714  mzpcompact2  42739  diophrw  42746  monotuz  42929  monotoddzz  42931  oddcomabszz  42932  flcidc  43158  nzss  44312  pm14.122b  44418  sbiota1  44429  fiiuncl  45004  axccdom  45164  axccd  45171  monoords  45247  fperiodmullem  45253  0ellimcdiv  45604  cncfperiod  45834  icccncfext  45842  fperdvper  45874  dvnmul  45898  dvnprodlem2  45902  iblspltprt  45928  itgspltprt  45934  stoweidlem4  45959  stoweidlem6  45961  stoweidlem8  45963  stoweidlem15  45970  stoweidlem16  45971  stoweidlem19  45974  stoweidlem20  45975  stoweidlem22  45977  stoweidlem23  45978  stoweidlem27  45982  stoweidlem30  45985  stoweidlem32  45987  stoweidlem34  45989  stoweidlem42  45997  stoweidlem48  46003  fourierdlem11  46073  fourierdlem16  46078  fourierdlem21  46083  fourierdlem41  46103  fourierdlem42  46104  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem68  46129  fourierdlem72  46133  fourierdlem76  46137  fourierdlem79  46140  fourierdlem81  46142  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  sge0f1o  46337  sge0p1  46369  hoidmvlelem4  46553  smfpimcclem  46762  funressnmo  46995  aiota0def  47045  csbafv12g  47086  csbaovg  47129  csbafv212g  47168  funressndmafv2rn  47172  funressnbrafv2  47193  funbrafv2  47196