Theorem vtoclg 3455

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   ∈ wcel 2155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-12 2213  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-v 3389

This theorem is referenced by:  vtoclbg  3456  moeq3  3575  mo2icl  3577  nelrdva  3609  sbctt  3690  sbcnestgf  4186  csbun  4201  csbin  4202  csbif  4328  prel12gOLD  4567  unisngOLD  4641  inex1g  4990  ssexg  4993  pwexg  5042  snex  5092  prex  5093  opth  5128  csbopab  5197  csbopabgALT  5198  vtoclr  5358  resieq  5605  csbima12  5687  dmsnsnsn  5819  dfpred3g  5898  predbrg  5907  preddowncl  5914  ordelord  5952  iota5  6078  csbiota  6088  funmo  6111  funimaexg  6180  fconstg  6301  funbrfv  6448  fvelimab  6468  ssimaexg  6479  fvelrn  6568  fsn2g  6622  isoselem  6809  csbriota  6841  csbov123  6909  ovg  7023  caovmo  7095  uniexg  7179  fnse  7522  onfununi  7668  rdg0g  7753  ensn1g  8251  fundmeng  8261  xpdom2g  8289  canth2g  8347  php2  8378  canthwdom  8717  zfregcl  8732  elirr  8735  tcvalg  8855  tz9.13g  8896  rankvalg  8921  ranklim  8948  r1pwALT  8950  rankuni2b  8957  rankuni  8967  cfslb2n  9369  itunitc1  9521  itunitc  9522  ituniiun  9523  hsmex  9533  axdc2lem  9549  ac7g  9575  ac6sg  9589  numthcor  9595  weth  9596  fodomg  9624  pwfseqlem4  9763  rankcf  9878  nqereu  10030  prnmax  10096  prlem936  10148  ltord1  10833  xmulasslem  12327  axdc4uz  13001  relexpind  14021  climshft  14524  telfsumo  14750  fsumparts  14754  lcmgcdlem  15532  mreacs  16517  dprdval  18598  fiinopn  20913  neiptoptop  21143  neiptopnei  21144  pt1hmeo  21817  isfildlem  21868  alexsublem  22055  ustuqtop4  22255  voliunlem3  23527  dvbsss  23874  dvfsumlem2  23998  acunirnmpt  29780  acunirnmpt2  29781  acunirnmpt2f  29782  carsgsigalem  30696  carsgclctunlem2  30700  carsgclctun  30702  pmeasmono  30705  pmeasadd  30706  sitgclg  30723  mclsrcl  31775  iota5f  31922  shftvalg  31933  dfrdg2  32015  fvsingle  32342  fullfunfv  32369  ranksng  32589  rankelg  32590  rankpwg  32591  rankeq1o  32593  csbdif  33482  mblfinlem3  33755  ismrer1  33942  mzpclall  37786  mzpcompact2  37811  diophrw  37818  monotuz  38001  monotoddzz  38003  oddcomabszz  38004  flcidc  38239  csbcog  38435  nzss  39010  pm14.122b  39117  sbiota1  39128  csbingOLD  39543  fiiuncl  39721  axccdom  39897  axccd  39907  monoords  39986  fperiodmullem  39992  0ellimcdiv  40355  cncfperiod  40566  icccncfext  40574  fperdvper  40607  dvnmul  40632  dvnprodlem2  40636  iblspltprt  40662  itgspltprt  40668  stoweidlem4  40694  stoweidlem6  40696  stoweidlem8  40698  stoweidlem15  40705  stoweidlem16  40706  stoweidlem19  40709  stoweidlem20  40710  stoweidlem22  40712  stoweidlem23  40713  stoweidlem27  40717  stoweidlem30  40720  stoweidlem32  40722  stoweidlem34  40724  stoweidlem42  40732  stoweidlem48  40738  fourierdlem11  40808  fourierdlem16  40813  fourierdlem21  40818  fourierdlem41  40838  fourierdlem42  40839  fourierdlem46  40842  fourierdlem48  40844  fourierdlem49  40845  fourierdlem50  40846  fourierdlem68  40864  fourierdlem72  40868  fourierdlem76  40872  fourierdlem79  40875  fourierdlem81  40877  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  fourierdlem92  40888  fourierdlem97  40893  fourierdlem103  40899  fourierdlem104  40900  fourierdlem111  40907  sge0f1o  41072  sge0p1  41104  hoidmvlelem4  41288  smfpimcclem  41489  funressnmo  41659  aiota0def  41672  csbafv12g  41720  csbaovg  41763  csbafv212g  41802  funressndmafv2rn  41806  funressnbrafv2  41827  funbrafv2  41830