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  3701  moeq3  3708  mo2icl  3710  sbcim1  3833  sbctt  3853  csbconstg  3912  sbcnestgfw  4418  sbcnestgf  4423  csbun  4438  csbin  4439  csbdif  4527  csbif  4585  axrep6g  5293  inex1g  5319  ssexg  5323  pwexg  5376  prex  5432  sels  5438  opth  5476  csbopab  5555  csbopabgALT  5556  vtoclr  5738  resieq  5991  csbima12  6076  dmsnsnsn  6217  csbcog  6294  dfpred3g  6310  predbrg  6320  preddowncl  6331  ordelord  6384  iota5  6524  csbiota  6534  funmoOLD  6562  funimaexgOLD  6633  fconstg  6776  funbrfv  6940  fvelimab  6962  ssimaexg  6975  fvelrn  7076  isoselem  7335  csbriota  7378  csbov123  7448  ovg  7569  caovmo  7641  uniexg  7727  fnse  8116  onfununi  8338  rdg0g  8424  ensn1g  9016  fundmeng  9029  xpdom2g  9065  canth2g  9128  ssfi  9170  php2OLD  9220  canthwdom  9571  zfregcl  9586  elirr  9589  ttrclselem2  9718  tcvalg  9730  tz9.13g  9784  rankvalg  9809  ranklim  9836  r1pwALT  9838  rankuni2b  9845  rankuni  9855  cfslb2n  10260  itunitc1  10412  itunitc  10413  ituniiun  10414  hsmex  10424  axdc2lem  10440  ac7g  10466  ac6sg  10480  numthcor  10486  weth  10487  pwfseqlem4  10654  rankcf  10769  nqereu  10921  prnmax  10987  prlem936  11039  ltord1  11737  xmulasslem  13261  axdc4uz  13946  relexpind  15008  climshft  15517  telfsumo  15745  fsumparts  15749  lcmgcdlem  16540  mreacs  17599  dprdval  19868  fiinopn  22395  neiptoptop  22627  neiptopnei  22628  pt1hmeo  23302  isfildlem  23353  alexsublem  23540  ustuqtop4  23741  voliunlem3  25061  dvbsss  25411  dvfsumlem2  25536  acunirnmpt  31872  acunirnmpt2  31873  acunirnmpt2f  31874  carsgsigalem  33303  carsgclctunlem2  33307  carsgclctun  33309  pmeasmono  33312  pmeasadd  33313  sitgclg  33330  mclsrcl  34541  iota5f  34682  shftvalg  34690  dfrdg2  34756  fvsingle  34881  fullfunfv  34908  ranksng  35128  rankelg  35129  rankpwg  35130  rankeq1o  35132  gg-dvfsumlem2  35172  bj-adjg1  35913  mblfinlem3  36516  ismrer1  36695  mzpclall  41451  mzpcompact2  41476  diophrw  41483  monotuz  41666  monotoddzz  41668  oddcomabszz  41669  flcidc  41902  nzss  43062  pm14.122b  43168  sbiota1  43179  fiiuncl  43738  axccdom  43907  axccd  43914  monoords  43994  fperiodmullem  44000  0ellimcdiv  44352  cncfperiod  44582  icccncfext  44590  fperdvper  44622  dvnmul  44646  dvnprodlem2  44650  iblspltprt  44676  itgspltprt  44682  stoweidlem4  44707  stoweidlem6  44709  stoweidlem8  44711  stoweidlem15  44718  stoweidlem16  44719  stoweidlem19  44722  stoweidlem20  44723  stoweidlem22  44725  stoweidlem23  44726  stoweidlem27  44730  stoweidlem30  44733  stoweidlem32  44735  stoweidlem34  44737  stoweidlem42  44745  stoweidlem48  44751  fourierdlem11  44821  fourierdlem16  44826  fourierdlem21  44831  fourierdlem41  44851  fourierdlem42  44852  fourierdlem46  44855  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem68  44877  fourierdlem72  44881  fourierdlem76  44885  fourierdlem79  44888  fourierdlem81  44890  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem92  44901  fourierdlem97  44906  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  sge0f1o  45085  sge0p1  45117  hoidmvlelem4  45301  smfpimcclem  45510  funressnmo  45743  aiota0def  45791  csbafv12g  45832  csbaovg  45875  csbafv212g  45914  funressndmafv2rn  45918  funressnbrafv2  45939  funbrafv2  45942