Theorem vtoclg 3239

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  vtoclbg  3240  moeq3  3350  mo2icl  3352  nelrdva  3384  sbctt  3467  sbcnestgf  3947  csbun  3961  csbin  3962  csbif  4088  prnzgOLD  4255  sneqrgOLD  4313  prel12g  4327  unisng  4388  trssOLD  4690  inex1g  4729  ssexg  4732  pwexg  4776  snex  4835  prex  4836  opth  4871  csbopab  4932  csbopabgALT  4933  vtoclr  5086  resieq  5327  csbima12  5402  dmsnsnsn  5531  dfpred3g  5608  predbrg  5617  preddowncl  5624  ordelord  5662  iota5  5788  csbiota  5797  funmo  5820  funimaexg  5889  fconstg  6005  funbrfv  6144  fvelimab  6163  ssimaexg  6174  fvelrn  6260  fsn2g  6311  isoselem  6491  csbriota  6523  csbov123  6585  ovg  6697  caovmo  6769  uniexg  6853  fnse  7181  onfununi  7325  rdg0g  7410  ensn1g  7907  fundmeng  7917  xpdom2g  7941  canth2g  7999  map2xp  8015  mapdom3  8017  php2  8030  canthwdom  8367  zfregcl  8382  elirr  8388  tcvalg  8497  tz9.13g  8538  rankvalg  8563  ranklim  8590  r1pwALT  8592  rankuni2b  8599  rankuni  8609  cfslb2n  8973  itunitc1  9125  itunitc  9126  ituniiun  9127  hsmex  9137  axdc2lem  9153  ac7g  9179  ac6sg  9193  numthcor  9199  weth  9200  fodomg  9228  pwfseqlem4  9363  pwxpndom2  9366  rankcf  9478  nqereu  9630  prnmax  9696  prlem936  9748  ltord1  10433  xmulasslem  11987  axdc4uz  12645  relexpind  13652  climshft  14155  telfsumo  14375  fsumparts  14379  lcmgcdlem  15157  mreacs  16142  dprdval  18225  fiinopn  20531  neiptoptop  20745  neiptopnei  20746  pt1hmeo  21419  isfildlem  21471  alexsublem  21658  ustuqtop4  21858  voliunlem3  23127  dvbsss  23472  dvfsumlem2  23594  1pthoncl  26122  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  carsgsigalem  29704  carsgclctunlem2  29708  carsgclctun  29710  pmeasmono  29713  pmeasadd  29714  sitgclg  29731  mclsrcl  30712  iota5f  30861  shftvalg  30870  dfrdg2  30945  fvsingle  31197  fullfunfv  31224  ranksng  31444  rankelg  31445  rankpwg  31446  rankeq1o  31448  csbdif  32347  mblfinlem3  32618  ismrer1  32807  mzpclall  36308  mzpcompact2  36333  diophrw  36340  monotuz  36524  monotoddzz  36526  oddcomabszz  36527  flcidc  36763  csbcog  36960  nzss  37538  pm14.122b  37646  sbiota1  37657  csbingOLD  38076  fiiuncl  38259  axccdom  38411  axccd  38424  monoords  38452  fperiodmullem  38458  0ellimcdiv  38716  cncfperiod  38764  icccncfext  38773  fperdvper  38808  dvnmul  38833  dvnprodlem2  38837  iblspltprt  38865  itgspltprt  38871  stoweidlem4  38897  stoweidlem6  38899  stoweidlem8  38901  stoweidlem15  38908  stoweidlem16  38909  stoweidlem19  38912  stoweidlem20  38913  stoweidlem22  38915  stoweidlem23  38916  stoweidlem27  38920  stoweidlem30  38923  stoweidlem32  38925  stoweidlem34  38927  stoweidlem42  38935  stoweidlem48  38941  fourierdlem11  39011  fourierdlem16  39016  fourierdlem21  39021  fourierdlem41  39041  fourierdlem42  39042  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem68  39067  fourierdlem72  39071  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  sge0f1o  39275  sge0p1  39307  hoidmvlelem4  39488  csbafv12g  39866  csbaovg  39909