MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclga Structured version   Unicode version

Theorem vtoclga 3025
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtoclga.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtoclga.2  |-  ( x  e.  B  ->  ph )
Assertion
Ref Expression
vtoclga  |-  ( A  e.  B  ->  ps )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem vtoclga
StepHypRef Expression
1 nfcv 2569 . 2  |-  F/_ x A
2 nfv 1672 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3024 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964
This theorem is referenced by:  vtoclri  3036  ssuni  4101  disjxiun  4277  opabiota  5742  fvmpt3  5765  fvmptss  5770  fnressn  5881  fressnfv  5883  caovord  6263  caovmo  6289  ordunisuc  6432  tfis3  6457  onfununi  6788  smogt  6814  tfrlem1  6821  tz7.44-1  6848  tz7.44-2  6849  tz7.44-3  6850  nnacl  7038  nnmcl  7039  nnecl  7040  nnacom  7044  nnaass  7049  nndi  7050  nnmass  7051  nnmsucr  7052  nnmcom  7053  nnmordi  7058  ixpfn  7257  findcard  7539  findcard2  7540  marypha1  7672  cantnfle  7867  cantnflem1  7885  cantnfleOLD  7897  cantnflem1OLD  7908  cnfcom  7921  cnfcomOLD  7929  fseqenlem1  8182  ackbij1lem5  8381  ackbij1lem8  8384  cardcf  8409  cfsmolem  8427  wunex2  8893  ingru  8970  recrecnq  9124  prlem934  9190  nn1suc  10331  uzind4s2  10903  rpnnen1  10972  cnref1o  10974  xmulasslem  11236  om2uzsuci  11755  expcl2lem  11861  hashmap  12181  hashpw  12182  seqcoll  12200  climub  13123  climserle  13124  sumrblem  13172  fsumcvg  13173  summolem2a  13176  infcvgaux2i  13303  divalglem8  13587  bezoutlem1  13705  alginv  13733  algcvg  13734  algcvga  13737  algfx  13738  isprm2lem  13753  prmind2  13757  prmpwdvds  13948  cnextfvval  19479  xrsxmet  20228  xrhmeo  20360  cmetcaulem  20641  bcth3  20684  itg2addlem  21078  taylfval  21709  sinord  21875  logexprlim  22449  lgsdir2lem4  22550  hlim2  24417  elnlfn  25155  lnconi  25260  chirredlem3  25619  chirredlem4  25620  cnre2csqlem  26194  eulerpartlemsf  26590  eulerpartlemn  26612  subfacp1lem1  26915  prodfn0  27256  prodfrec  27257  prodrblem  27289  fprodcvg  27290  prodmolem2a  27294  wfis3  27523  frins3  27559  wfr2  27588  findreccl  28147  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  ftc1anclem3  28313  ftc1anclem8  28318  nn0prpwlem  28361  sdclem2  28482  iscringd  28643  zindbi  29132  fmuldfeq  29609  stoweidlem2  29643  stoweidlem17  29658  stoweidlem21  29662  stoweidlem34  29675  stoweidlem42  29683  stoweidlem43  29684  stoweidlem48  29689  stoweidlem51  29692  wallispi  29711  bnj1321  31720  bnj1418  31733  renegclALT  32187
  Copyright terms: Public domain W3C validator