Theorem vtoclg 3554

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108

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 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816

This theorem is referenced by:  vtoclbg  3557  vtocl2g  3574  vtocl3g  3575  vtoclga  3577  nelrdva  3711  moeq3  3718  mo2icl  3720  sbcim1  3842  sbctt  3860  csbconstg  3918  sbcnestgfw  4421  sbcnestgf  4426  csbun  4441  csbin  4442  csbdif  4524  csbif  4583  axrep6g  5290  inex1g  5319  ssexg  5323  pwexg  5378  prex  5437  sels  5443  opth  5481  csbopab  5560  csbopabgALT  5561  vtoclr  5748  resieq  6008  csbima12  6097  dmsnsnsn  6240  csbcog  6317  dfpred3g  6333  preddowncl  6353  ordelord  6406  iota5  6544  csbiota  6554  funmoOLD  6582  funimaexgOLD  6654  fconstg  6795  funbrfv  6957  fvelimab  6981  ssimaexg  6995  fvelrn  7096  isoselem  7361  csbriota  7403  csbov123  7475  ovg  7598  caovmo  7670  uniexg  7760  fnse  8158  onfununi  8381  rdg0g  8467  ensn1g  9062  fundmeng  9072  xpdom2g  9108  canth2g  9171  ssfi  9213  php2OLD  9260  canthwdom  9619  zfregcl  9634  elirr  9637  ttrclselem2  9766  tcvalg  9778  tz9.13g  9832  rankvalg  9857  ranklim  9884  r1pwALT  9886  rankuni2b  9893  rankuni  9903  cfslb2n  10308  itunitc1  10460  itunitc  10461  ituniiun  10462  hsmex  10472  axdc2lem  10488  ac7g  10514  ac6sg  10528  numthcor  10534  weth  10535  rankcf  10817  nqereu  10969  prnmax  11035  prlem936  11087  ltord1  11789  xmulasslem  13327  axdc4uz  14025  relexpind  15103  climshft  15612  telfsumo  15838  fsumparts  15842  lcmgcdlem  16643  mreacs  17701  dprdval  20023  fiinopn  22907  neiptoptop  23139  neiptopnei  23140  pt1hmeo  23814  isfildlem  23865  alexsublem  24052  ustuqtop4  24253  voliunlem3  25587  dvbsss  25937  dvfsumlem2  26067  dvfsumlem2OLD  26068  acunirnmpt  32669  acunirnmpt2  32670  acunirnmpt2f  32671  carsgsigalem  34317  carsgclctunlem2  34321  carsgclctun  34323  pmeasmono  34326  pmeasadd  34327  sitgclg  34344  mclsrcl  35566  iota5f  35724  shftvalg  35732  dfrdg2  35796  fvsingle  35921  fullfunfv  35948  ranksng  36168  rankelg  36169  rankpwg  36170  rankeq1o  36172  bj-adjg1  37044  mblfinlem3  37666  ismrer1  37845  mzpclall  42738  mzpcompact2  42763  diophrw  42770  monotuz  42953  monotoddzz  42955  oddcomabszz  42956  flcidc  43182  nzss  44336  pm14.122b  44442  sbiota1  44453  fiiuncl  45070  axccdom  45227  axccd  45234  monoords  45309  fperiodmullem  45315  0ellimcdiv  45664  cncfperiod  45894  icccncfext  45902  fperdvper  45934  dvnmul  45958  dvnprodlem2  45962  iblspltprt  45988  itgspltprt  45994  stoweidlem4  46019  stoweidlem6  46021  stoweidlem8  46023  stoweidlem15  46030  stoweidlem16  46031  stoweidlem19  46034  stoweidlem20  46035  stoweidlem22  46037  stoweidlem23  46038  stoweidlem27  46042  stoweidlem30  46045  stoweidlem32  46047  stoweidlem34  46049  stoweidlem42  46057  stoweidlem48  46063  fourierdlem11  46133  fourierdlem16  46138  fourierdlem21  46143  fourierdlem41  46163  fourierdlem42  46164  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem68  46189  fourierdlem72  46193  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  sge0f1o  46397  sge0p1  46429  hoidmvlelem4  46613  smfpimcclem  46822  funressnmo  47058  aiota0def  47108  csbafv12g  47149  csbaovg  47192  csbafv212g  47231  funressndmafv2rn  47235  funressnbrafv2  47256  funbrafv2  47259