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

Theorem rspcva 3042
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcva  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcva
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 3040 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 419 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   A.wral 2697
This theorem is referenced by:  tfisi  4830  suppssov1  6294  caofinvl  6323  boxriin  7096  boxcutc  7097  marypha1lem  7430  marypha1  7431  supmo  7449  wemaplem2  7508  unwdomg  7544  noinfepOLD  7607  isinffi  7871  dfac9  8008  sornom  8149  fin23lem11  8189  fin1a2lem13  8284  axdc3lem2  8323  winalim2  8563  grothac  8697  nqereu  8798  infmrcl  9979  nnsub  10030  zextle  10335  xrsupsslem  10877  xrinfmsslem  10878  supxrunb1  10890  supxrunb2  10891  injresinjlem  11191  faclbnd4lem4  11579  rexuz3  12144  cau3lem  12150  caubnd2  12153  o1co  12372  climcn1  12377  incexclem  12608  dvdsext  12892  prdsbasprj  13686  mreintcl  13812  isacs2  13870  acsfiel  13871  isdrs2  14388  lubid  14431  acsdrsel  14585  isacs4lem  14586  isacs5lem  14587  acsdrscl  14588  acsficl  14589  mgmidmo  14685  gsumval2  14775  odeq  15180  gexid  15207  mplind  16554  cmpsublem  17454  cmpsub  17455  hauscmplem  17461  cmpfii  17464  ptpjcn  17635  isufil2  17932  ufileu  17943  cfiluweak  18317  cuspcvg  18323  lpbl  18525  lmmbr  19203  caussi  19242  evlslem1  19928  mdeglt  19980  deg1lt  20012  ply1divex  20051  plyco0  20103  dgrco  20185  emcllem7  20832  isppw2  20890  pntleme  21294  pntlemp  21296  nbcusgra  21464  uvtxnbgra  21494  wlkdvspthlem  21599  grpoidinvlem3  21786  grpoideu  21789  lnconi  23528  ishashinf  24151  kerf1hrm  24254  tpr2rico  24302  ofcfeqd2  24476  0elsiga  24489  sigaclci  24507  dya2icoseg2  24620  derangsn  24848  wfr3g  25529  frr3g  25573  mblfinlem  26234  ftc1anc  26278  fdc  26440  bndss  26486  isdrngo2  26565  divrngidl  26629  maxidlmax  26644  ismrcd1  26743  nacsfg  26750  isnacs3  26755  nacsfix  26757  mzpcl1  26777  mzpcl2  26778  mzpcong  27028  dnnumch1  27110  fnwe2lem2  27117  aomclem1  27120  aomclem4  27123  aomclem6  27125  lnr2i  27288  hbtlem5  27300  hbt  27302  frgraunss  28322  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  frgrancvvdeqlem4  28359  frgraregorufr  28379  cdleme0nex  31024  dihglblem2N  32029  hgmapvs  32629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950
  Copyright terms: Public domain W3C validator