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

Theorem vtoclga 3142
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 2582 . 2  |-  F/_ x A
2 nfv 1751 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3141 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080
This theorem is referenced by:  vtoclri  3153  ssuni  4235  disjxiun  4414  wfis3  5431  opabiota  5935  fvmpt3  5959  fvmptss  5965  fnressn  6082  fressnfv  6084  caovord  6485  caovmo  6511  ordunisuc  6664  tfis3  6689  wfr2a  7052  onfununi  7059  smogt  7085  tz7.44-1  7123  tz7.44-2  7124  tz7.44-3  7125  nnacl  7311  nnmcl  7312  nnecl  7313  nnacom  7317  nnaass  7322  nndi  7323  nnmass  7324  nnmsucr  7325  nnmcom  7326  nnmordi  7331  ixpfn  7527  findcard  7807  findcard2  7808  marypha1  7945  cantnfle  8166  cantnflem1  8184  cnfcom  8195  fseqenlem1  8444  ackbij1lem5  8643  ackbij1lem8  8646  cardcf  8671  cfsmolem  8689  wunex2  9152  ingru  9229  recrecnq  9381  prlem934  9447  nn1suc  10619  uzind4s2  11209  rpnnen1  11284  cnref1o  11286  xmulasslem  11560  om2uzsuci  12148  expcl2lem  12270  hashmap  12591  hashpw  12592  seqcoll  12610  climub  13692  climserle  13693  sumrblem  13744  fsumcvg  13745  summolem2a  13748  infcvgaux2i  13883  prodfn0  13917  prodfrec  13918  prodrblem  13950  fprodcvg  13951  prodmolem2a  13955  divalglem8  14345  bezoutlem1  14466  alginv  14494  algcvg  14495  algcvga  14498  algfx  14499  isprm2lem  14591  prmind2  14595  prmpwdvds  14800  cnextfvval  21004  xrsxmet  21731  xrhmeo  21863  cmetcaulem  22144  bcth3  22185  itg2addlem  22590  taylfval  23176  sinord  23345  logexprlim  24013  lgsdir2lem4  24114  hlim2  26677  elnlfn  27413  lnconi  27518  chirredlem3  27877  chirredlem4  27878  cnre2csqlem  28552  eulerpartlemsf  29015  eulerpartlemn  29037  bnj1321  29621  bnj1418  29634  subfacp1lem1  29687  frins3  30273  nn0prpwlem  30760  findreccl  30895  mptsnunlem  31471  poimirlem22  31666  poimirlem26  31670  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  ftc1anclem3  31723  ftc1anclem8  31728  sdclem2  31775  iscringd  31936  renegclALT  32244  zindbi  35504  fmuldfeq  37237  sumnnodd  37286  iblspltprt  37423  stoweidlem2  37435  stoweidlem17  37450  stoweidlem21  37454  stoweidlem43  37477  stoweidlem51  37485  wallispi  37505
  Copyright terms: Public domain W3C validator