Theorem vtoclg 3266

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

Hypotheses

Ref	Expression
vtoclg.1	|- ( x = A -> ( ph <-> ps ) )
vtoclg.2	|- ph

Assertion

Ref	Expression
vtoclg	|- ( A e. V -> ps )

Distinct variable groups:   x, A   ps, x

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ps
2		vtoclg.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3		vtoclg.2	. 2 |- ph
4	1, 2, 3	vtoclg1f 3265	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  vtoclbg  3267  moeq3  3383  mo2icl  3385  nelrdva  3417  sbctt  3500  sbcnestgf  3995  csbun  4009  csbin  4010  csbif  4138  prnzgOLD  4312  sneqrgOLD  4373  prel12g  4387  unisng  4452  trssOLD  4762  inex1g  4801  ssexg  4804  pwexg  4850  snex  4908  prex  4909  opth  4945  csbopab  5008  csbopabgALT  5009  vtoclr  5164  resieq  5407  csbima12  5483  dmsnsnsn  5613  dfpred3g  5691  predbrg  5700  preddowncl  5707  ordelord  5745  iota5  5871  csbiota  5881  funmo  5904  funimaexg  5975  fconstg  6092  funbrfv  6234  fvelimab  6253  ssimaexg  6264  fvelrn  6352  fsn2g  6405  isoselem  6591  csbriota  6623  csbov123  6687  ovg  6799  caovmo  6871  uniexg  6955  fnse  7294  onfununi  7438  rdg0g  7523  ensn1g  8021  fundmeng  8031  xpdom2g  8056  canth2g  8114  map2xp  8130  mapdom3  8132  php2  8145  canthwdom  8484  zfregcl  8499  elirr  8505  tcvalg  8614  tz9.13g  8655  rankvalg  8680  ranklim  8707  r1pwALT  8709  rankuni2b  8716  rankuni  8726  cfslb2n  9090  itunitc1  9242  itunitc  9243  ituniiun  9244  hsmex  9254  axdc2lem  9270  ac7g  9296  ac6sg  9310  numthcor  9316  weth  9317  fodomg  9345  pwfseqlem4  9484  pwxpndom2  9487  rankcf  9599  nqereu  9751  prnmax  9817  prlem936  9869  ltord1  10554  xmulasslem  12115  axdc4uz  12783  relexpind  13804  climshft  14307  telfsumo  14534  fsumparts  14538  lcmgcdlem  15319  mreacs  16319  dprdval  18402  fiinopn  20706  neiptoptop  20935  neiptopnei  20936  pt1hmeo  21609  isfildlem  21661  alexsublem  21848  ustuqtop4  22048  voliunlem3  23320  dvbsss  23666  dvfsumlem2  23790  acunirnmpt  29459  acunirnmpt2  29460  acunirnmpt2f  29461  carsgsigalem  30377  carsgclctunlem2  30381  carsgclctun  30383  pmeasmono  30386  pmeasadd  30387  sitgclg  30404  mclsrcl  31458  iota5f  31606  shftvalg  31617  dfrdg2  31701  fvsingle  32027  fullfunfv  32054  ranksng  32274  rankelg  32275  rankpwg  32276  rankeq1o  32278  csbdif  33171  mblfinlem3  33448  ismrer1  33637  mzpclall  37290  mzpcompact2  37315  diophrw  37322  monotuz  37506  monotoddzz  37508  oddcomabszz  37509  flcidc  37744  csbcog  37941  nzss  38516  pm14.122b  38624  sbiota1  38635  csbingOLD  39054  fiiuncl  39234  axccdom  39416  axccd  39429  monoords  39511  fperiodmullem  39517  0ellimcdiv  39881  cncfperiod  40092  icccncfext  40100  fperdvper  40133  dvnmul  40158  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  stoweidlem4  40221  stoweidlem6  40223  stoweidlem8  40225  stoweidlem15  40232  stoweidlem16  40233  stoweidlem19  40236  stoweidlem20  40237  stoweidlem22  40239  stoweidlem23  40240  stoweidlem27  40244  stoweidlem30  40247  stoweidlem32  40249  stoweidlem34  40251  stoweidlem42  40259  stoweidlem48  40265  fourierdlem11  40335  fourierdlem16  40340  fourierdlem21  40345  fourierdlem41  40365  fourierdlem42  40366  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem68  40391  fourierdlem72  40395  fourierdlem76  40399  fourierdlem79  40402  fourierdlem81  40404  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  sge0f1o  40599  sge0p1  40631  hoidmvlelem4  40812  smfpimcclem  41013  csbafv12g  41217  csbaovg  41260