Theorem vtoclg 3567

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  vtoclbg  3568  vtocl2g  3571  vtoclga  3573  nelrdva  3695  moeq3  3702  mo2icl  3704  sbctt  3843  sbcnestgfw  4369  sbcnestgf  4374  csbun  4389  csbin  4390  csbif  4521  inex1g  5222  ssexg  5226  pwexg  5278  snex  5331  prex  5332  opth  5367  csbopab  5441  csbopabgALT  5442  vtoclr  5614  resieq  5863  csbima12  5946  dmsnsnsn  6076  dfpred3g  6158  predbrg  6167  preddowncl  6174  ordelord  6212  iota5  6337  csbiota  6347  funmo  6370  funimaexg  6439  fconstg  6565  funbrfv  6715  fvelimab  6736  ssimaexg  6748  fvelrn  6843  isoselem  7093  csbriota  7128  csbov123  7197  ovg  7312  caovmo  7384  uniexg  7465  fnse  7826  onfununi  7977  rdg0g  8062  ensn1g  8573  fundmeng  8583  xpdom2g  8612  canth2g  8670  php2  8701  canthwdom  9042  zfregcl  9057  elirr  9060  tcvalg  9179  tz9.13g  9220  rankvalg  9245  ranklim  9272  r1pwALT  9274  rankuni2b  9281  rankuni  9291  cfslb2n  9689  itunitc1  9841  itunitc  9842  ituniiun  9843  hsmex  9853  axdc2lem  9869  ac7g  9895  ac6sg  9909  numthcor  9915  weth  9916  fodomg  9944  pwfseqlem4  10083  rankcf  10198  nqereu  10350  prnmax  10416  prlem936  10468  ltord1  11165  xmulasslem  12677  axdc4uz  13351  relexpind  14422  climshft  14932  telfsumo  15156  fsumparts  15160  lcmgcdlem  15949  mreacs  16928  dprdval  19124  fiinopn  21508  neiptoptop  21738  neiptopnei  21739  pt1hmeo  22413  isfildlem  22464  alexsublem  22651  ustuqtop4  22852  voliunlem3  24152  dvbsss  24499  dvfsumlem2  24623  acunirnmpt  30403  acunirnmpt2  30404  acunirnmpt2f  30405  carsgsigalem  31573  carsgclctunlem2  31577  carsgclctun  31579  pmeasmono  31582  pmeasadd  31583  sitgclg  31600  mclsrcl  32808  iota5f  32955  shftvalg  32963  dfrdg2  33040  fvsingle  33381  fullfunfv  33408  ranksng  33628  rankelg  33629  rankpwg  33630  rankeq1o  33632  csbdif  34605  mblfinlem3  34930  ismrer1  35115  mzpclall  39322  mzpcompact2  39347  diophrw  39354  monotuz  39536  monotoddzz  39538  oddcomabszz  39539  flcidc  39772  csbcog  39992  nzss  40647  pm14.122b  40753  sbiota1  40764  fiiuncl  41325  axccdom  41485  axccd  41493  monoords  41562  fperiodmullem  41568  0ellimcdiv  41928  cncfperiod  42160  icccncfext  42168  fperdvper  42201  dvnmul  42226  dvnprodlem2  42230  iblspltprt  42256  itgspltprt  42262  stoweidlem4  42288  stoweidlem6  42290  stoweidlem8  42292  stoweidlem15  42299  stoweidlem16  42300  stoweidlem19  42303  stoweidlem20  42304  stoweidlem22  42306  stoweidlem23  42307  stoweidlem27  42311  stoweidlem30  42314  stoweidlem32  42316  stoweidlem34  42318  stoweidlem42  42326  stoweidlem48  42332  fourierdlem11  42402  fourierdlem16  42407  fourierdlem21  42412  fourierdlem41  42432  fourierdlem42  42433  fourierdlem46  42436  fourierdlem48  42438  fourierdlem49  42439  fourierdlem50  42440  fourierdlem68  42458  fourierdlem72  42462  fourierdlem76  42466  fourierdlem79  42469  fourierdlem81  42471  fourierdlem89  42479  fourierdlem90  42480  fourierdlem91  42481  fourierdlem92  42482  fourierdlem97  42487  fourierdlem103  42493  fourierdlem104  42494  fourierdlem111  42501  sge0f1o  42663  sge0p1  42695  hoidmvlelem4  42879  smfpimcclem  43080  funressnmo  43280  aiota0def  43293  csbafv12g  43335  csbaovg  43378  csbafv212g  43417  funressndmafv2rn  43421  funressnbrafv2  43442  funbrafv2  43445