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

Theorem vtoclga 3182
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 2629 . 2  |-  F/_ x A
2 nfv 1683 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3181 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120
This theorem is referenced by:  vtoclri  3193  ssuni  4273  disjxiun  4450  opabiota  5937  fvmpt3  5960  fvmptss  5965  fnressn  6084  fressnfv  6086  caovord  6481  caovmo  6507  ordunisuc  6662  tfis3  6687  onfununi  7024  smogt  7050  tfrlem1  7057  tz7.44-1  7084  tz7.44-2  7085  tz7.44-3  7086  nnacl  7272  nnmcl  7273  nnecl  7274  nnacom  7278  nnaass  7283  nndi  7284  nnmass  7285  nnmsucr  7286  nnmcom  7287  nnmordi  7292  ixpfn  7487  findcard  7771  findcard2  7772  marypha1  7906  cantnfle  8102  cantnflem1  8120  cantnfleOLD  8132  cantnflem1OLD  8143  cnfcom  8156  cnfcomOLD  8164  fseqenlem1  8417  ackbij1lem5  8616  ackbij1lem8  8619  cardcf  8644  cfsmolem  8662  wunex2  9128  ingru  9205  recrecnq  9357  prlem934  9423  nn1suc  10569  uzind4s2  11154  rpnnen1  11225  cnref1o  11227  xmulasslem  11489  om2uzsuci  12039  expcl2lem  12158  hashmap  12474  hashpw  12475  seqcoll  12493  climub  13464  climserle  13465  sumrblem  13513  fsumcvg  13514  summolem2a  13517  infcvgaux2i  13649  divalglem8  13934  bezoutlem1  14052  alginv  14080  algcvg  14081  algcvga  14084  algfx  14085  isprm2lem  14100  prmind2  14104  prmpwdvds  14298  cnextfvval  20433  xrsxmet  21182  xrhmeo  21314  cmetcaulem  21595  bcth3  21638  itg2addlem  22033  taylfval  22621  sinord  22787  logexprlim  23366  lgsdir2lem4  23467  hlim2  25932  elnlfn  26670  lnconi  26775  chirredlem3  27134  chirredlem4  27135  cnre2csqlem  27717  eulerpartlemsf  28123  eulerpartlemn  28145  subfacp1lem1  28448  prodfn0  28955  prodfrec  28956  prodrblem  28988  fprodcvg  28989  prodmolem2a  28993  wfis3  29222  frins3  29258  wfr2  29287  findreccl  29845  mblfinlem3  29980  mblfinlem4  29981  ismblfin  29982  ftc1anclem3  30019  ftc1anclem8  30024  nn0prpwlem  30067  sdclem2  30162  iscringd  30323  zindbi  30810  fmuldfeq  31456  sumnnodd  31495  cncfperiod  31540  icccncfext  31549  fperdvper  31571  iblspltprt  31614  itgspltprt  31620  stoweidlem2  31625  stoweidlem17  31640  stoweidlem21  31644  stoweidlem43  31666  stoweidlem51  31674  wallispi  31693  fourierdlem11  31741  fourierdlem42  31772  fourierdlem72  31802  fourierdlem81  31811  fourierdlem92  31822  bnj1321  33563  bnj1418  33576  renegclALT  34167
  Copyright terms: Public domain W3C validator