Theorem vtoclg 3486

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)

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		nfv 1873	. 2 ⊢ Ⅎ𝑥𝜓
2		vtoclg.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		vtoclg.2	. 2 ⊢ 𝜑
4	1, 2, 3	vtoclg1f 3485	1 ⊢ (𝐴 ∈ 𝑉 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-cleq 2771  df-clel 2846

This theorem is referenced by:  vtoclbg  3487  vtocl2g  3490  vtoclga  3493  nelrdva  3610  moeq3  3617  mo2icl  3619  sbctt  3747  sbcnestgf  4259  csbun  4274  csbin  4275  csbif  4405  inex1g  5080  ssexg  5083  pwexg  5132  snex  5188  prex  5189  opth  5225  csbopab  5294  csbopabgALT  5295  vtoclr  5465  resieq  5709  csbima12  5787  dmsnsnsn  5916  dfpred3g  5997  predbrg  6006  preddowncl  6013  ordelord  6051  iota5  6172  csbiota  6181  funmo  6204  funimaexg  6273  fconstg  6395  funbrfv  6546  fvelimab  6566  ssimaexg  6577  fvelrn  6669  isoselem  6917  csbriota  6949  csbov123  7017  ovg  7129  caovmo  7201  uniexg  7285  fnse  7632  onfununi  7782  rdg0g  7867  ensn1g  8371  fundmeng  8381  xpdom2g  8409  canth2g  8467  php2  8498  canthwdom  8838  zfregcl  8853  elirr  8856  tcvalg  8974  tz9.13g  9015  rankvalg  9040  ranklim  9067  r1pwALT  9069  rankuni2b  9076  rankuni  9086  cfslb2n  9488  itunitc1  9640  itunitc  9641  ituniiun  9642  hsmex  9652  axdc2lem  9668  ac7g  9694  ac6sg  9708  numthcor  9714  weth  9715  fodomg  9743  pwfseqlem4  9882  rankcf  9997  nqereu  10149  prnmax  10215  prlem936  10267  ltord1  10967  xmulasslem  12494  axdc4uz  13167  relexpind  14284  climshft  14794  telfsumo  15017  fsumparts  15021  lcmgcdlem  15806  mreacs  16787  dprdval  18875  fiinopn  21213  neiptoptop  21443  neiptopnei  21444  pt1hmeo  22118  isfildlem  22169  alexsublem  22356  ustuqtop4  22556  voliunlem3  23856  dvbsss  24203  dvfsumlem2  24327  acunirnmpt  30166  acunirnmpt2  30167  acunirnmpt2f  30168  carsgsigalem  31224  carsgclctunlem2  31228  carsgclctun  31230  pmeasmono  31233  pmeasadd  31234  sitgclg  31251  mclsrcl  32334  iota5f  32481  shftvalg  32489  dfrdg2  32567  fvsingle  32908  fullfunfv  32935  ranksng  33155  rankelg  33156  rankpwg  33157  rankeq1o  33159  csbdif  34054  mblfinlem3  34378  ismrer1  34564  mzpclall  38725  mzpcompact2  38750  diophrw  38757  monotuz  38940  monotoddzz  38942  oddcomabszz  38943  flcidc  39176  csbcog  39363  nzss  40071  pm14.122b  40178  sbiota1  40189  fiiuncl  40752  axccdom  40918  axccd  40927  monoords  40999  fperiodmullem  41005  0ellimcdiv  41367  cncfperiod  41598  icccncfext  41606  fperdvper  41639  dvnmul  41664  dvnprodlem2  41668  iblspltprt  41694  itgspltprt  41700  stoweidlem4  41726  stoweidlem6  41728  stoweidlem8  41730  stoweidlem15  41737  stoweidlem16  41738  stoweidlem19  41741  stoweidlem20  41742  stoweidlem22  41744  stoweidlem23  41745  stoweidlem27  41749  stoweidlem30  41752  stoweidlem32  41754  stoweidlem34  41756  stoweidlem42  41764  stoweidlem48  41770  fourierdlem11  41840  fourierdlem16  41845  fourierdlem21  41850  fourierdlem41  41870  fourierdlem42  41871  fourierdlem46  41874  fourierdlem48  41876  fourierdlem49  41877  fourierdlem50  41878  fourierdlem68  41896  fourierdlem72  41900  fourierdlem76  41904  fourierdlem79  41907  fourierdlem81  41909  fourierdlem89  41917  fourierdlem90  41918  fourierdlem91  41919  fourierdlem92  41920  fourierdlem97  41925  fourierdlem103  41931  fourierdlem104  41932  fourierdlem111  41939  sge0f1o  42101  sge0p1  42133  hoidmvlelem4  42317  smfpimcclem  42518  funressnmo  42693  aiota0def  42706  csbafv12g  42748  csbaovg  42791  csbafv212g  42830  funressndmafv2rn  42834  funressnbrafv2  42855  funbrafv2  42858