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

Theorem vtoclga 3170
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 2616 . 2  |-  F/_ x A
2 nfv 1712 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3169 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398    e. wcel 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108
This theorem is referenced by:  vtoclri  3181  ssuni  4257  disjxiun  4436  opabiota  5911  fvmpt3  5934  fvmptss  5940  fnressn  6059  fressnfv  6061  caovord  6459  caovmo  6485  ordunisuc  6640  tfis3  6665  onfununi  7004  smogt  7030  tz7.44-1  7064  tz7.44-2  7065  tz7.44-3  7066  nnacl  7252  nnmcl  7253  nnecl  7254  nnacom  7258  nnaass  7263  nndi  7264  nnmass  7265  nnmsucr  7266  nnmcom  7267  nnmordi  7272  ixpfn  7468  findcard  7751  findcard2  7752  marypha1  7886  cantnfle  8081  cantnflem1  8099  cantnfleOLD  8111  cantnflem1OLD  8122  cnfcom  8135  cnfcomOLD  8143  fseqenlem1  8396  ackbij1lem5  8595  ackbij1lem8  8598  cardcf  8623  cfsmolem  8641  wunex2  9105  ingru  9182  recrecnq  9334  prlem934  9400  nn1suc  10552  uzind4s2  11143  rpnnen1  11214  cnref1o  11216  xmulasslem  11480  om2uzsuci  12041  expcl2lem  12160  hashmap  12477  hashpw  12478  seqcoll  12496  climub  13566  climserle  13567  sumrblem  13615  fsumcvg  13616  summolem2a  13619  infcvgaux2i  13751  prodfn0  13785  prodfrec  13786  prodrblem  13818  fprodcvg  13819  prodmolem2a  13823  divalglem8  14142  bezoutlem1  14260  alginv  14288  algcvg  14289  algcvga  14292  algfx  14293  isprm2lem  14308  prmind2  14312  prmpwdvds  14506  cnextfvval  20731  xrsxmet  21480  xrhmeo  21612  cmetcaulem  21893  bcth3  21936  itg2addlem  22331  taylfval  22920  sinord  23087  logexprlim  23698  lgsdir2lem4  23799  hlim2  26307  elnlfn  27045  lnconi  27150  chirredlem3  27509  chirredlem4  27510  cnre2csqlem  28127  eulerpartlemsf  28562  eulerpartlemn  28584  subfacp1lem1  28887  wfis3  29535  frins3  29571  wfr2  29600  findreccl  30146  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  ftc1anclem3  30332  ftc1anclem8  30337  nn0prpwlem  30380  sdclem2  30475  iscringd  30636  zindbi  31121  fmuldfeq  31816  sumnnodd  31875  iblspltprt  32011  stoweidlem2  32023  stoweidlem17  32038  stoweidlem21  32042  stoweidlem43  32064  stoweidlem51  32072  wallispi  32091  bnj1321  34484  bnj1418  34497  renegclALT  35091
  Copyright terms: Public domain W3C validator