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

Theorem rspccva 3011
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspccva  |-  ( ( A. x  e.  B  ph 
/\  A  e.  B
)  ->  ps )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspccva
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 3008 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32impcom 420 1  |-  ( ( A. x  e.  B  ph 
/\  A  e.  B
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2666
This theorem is referenced by:  disjne  3633  seex  4505  foelrn  5847  fconstfv  5913  grprinvlem  6244  caofid0l  6291  caofid0r  6292  caofid1  6293  caofid2  6294  onnseq  6565  odi  6781  omsmolem  6855  fvixp  7026  unblem1  7318  ordiso2  7440  unwdomg  7508  ac5num  7873  acni2  7883  fodomacn  7893  iundom2g  8371  fpwwe2lem3  8464  eltsk2g  8582  tskpwss  8583  tskpw  8584  tsken  8585  prlem934  8866  ltord1  9509  leord1  9510  eqord1  9511  ltord2  9512  leord2  9513  eqord2  9514  supmul1  9929  seqcaopr2  11314  bccl  11568  hashbc  11657  limsupbnd2  12232  2clim  12321  climsup  12418  caurcvg2  12426  caucvgb  12428  isummulc2  12501  fsumtscopo2  12537  fsumparts  12540  incexclem  12571  isumshft  12574  climcndslem1  12584  climcndslem2  12585  supcvg  12590  geomulcvg  12608  mertenslem2  12617  mertens  12618  rpnnen2lem10  12778  dvdsprime  13047  iscatd2  13861  fuciso  14127  lubub  14501  lubl  14502  mgmlrid  14667  grpinvex  14775  issubg2  14914  issubg4  14916  nmzbi  14935  gagrpid  15026  cntzi  15083  sylow1lem3  15189  pgpfi  15194  slwispgp  15200  sylow2alem1  15206  dprdfcl  15526  ablfac2  15602  abveq0  15869  issrngd  15904  psrbagconf1o  16394  phllmhm  16818  ipcl  16819  ipeq0  16824  isphld  16840  ocvi  16851  elcls3  17102  neindisj2  17142  perfi  17173  cnima  17283  1stcfb  17461  1stcelcls  17477  llyi  17490  nllyi  17491  1stckgenlem  17538  ptbasin  17562  txcls  17589  ptcnp  17607  ufli  17899  tgpt0  18101  tsmsxplem2  18136  nrmmetd  18575  tngngp  18648  reperflem  18802  lebnumlem3  18941  htpyi  18952  htpycc  18958  phtpyi  18962  cfili  19174  cmetcvg  19191  caubl  19213  caublcls  19214  bcthlem2  19231  bcthlem3  19232  bcthlem4  19233  ovolicc2lem1  19366  ovolicc2lem5  19370  ovolicc2  19371  voliunlem3  19399  volsuplem  19402  uniioombllem2  19428  mbfima  19477  ismbfd  19485  ismbf3d  19499  mbfmullem  19570  itg2monolem1  19595  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  bddmulibl  19683  c1liplem1  19833  dvfsumle  19858  dvfsumabs  19860  dvfsumrlimf  19862  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlimge0  19867  dvfsum2  19871  ftc1lem6  19878  pf1ind  19928  ulmcau  20264  ulmdvlem1  20269  ulmdvlem3  20271  mtestbdd  20274  itgulm  20277  radcnvlem1  20282  abelthlem5  20304  abelthlem7  20307  areambl  20750  dchrisumlem2  21137  dchrvmasumiflem1  21148  pntpbnd1  21233  ostthlem1  21274  usgrcyclnl1  21580  eupaseg  21648  grpoidinvlem3  21747  grpoidinv  21749  grpoidinv2  21759  isgrp2d  21776  cmpidelt  21870  rngoid  21924  vcid  21983  minvecolem5  22336  hcaucvg  22641  hlimconvi  22646  lnopeq0i  23463  cnlnadjlem5  23527  csmdsymi  23790  difelsiga  24469  ballotlemfc0  24703  ballotlemfcc  24704  ptpcon  24873  cvmsdisj  24910  cvmshmeo  24911  snmlflim  24972  sinccvg  25063  dedekindle  25141  preddowncl  25410  brbtwn2  25748  ax5seglem1  25771  ax5seglem2  25772  ax5seglem9  25780  axcontlem4  25810  axcontlem12  25818  bpolycl  26002  bpolydif  26005  mblfinlem  26143  ovoliunnfl  26147  ex-ovoliunnfl  26148  voliunnfl  26149  volsupnfl  26150  mbfresfi  26152  itg2gt0cn  26159  bddiblnc  26174  ftc1cnnc  26178  locfinnei  26272  fnemeet1  26285  fnemeet2  26286  fnejoin1  26287  fnejoin2  26288  upixp  26321  filbcmb  26332  sdclem1  26337  seqpo  26341  incsequz2  26343  mettrifi  26353  caushft  26357  sstotbnd2  26373  heibor1lem  26408  heiborlem3  26412  heiborlem10  26419  heibor  26420  rrndstprj2  26430  limsuc2  27005  psgnunilem2  27286  cncmpmax  27570  climinf  27599  climsuse  27601  stoweidlem7  27623  stoweidlem15  27631  stoweidlem21  27637  stoweidlem31  27647  stoweidlem35  27651  stoweidlem36  27652  stoweidlem50  27666  stoweidlem57  27673  stoweidlem59  27675  wallispilem3  27683  usgreghash2spot  28172
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918
  Copyright terms: Public domain W3C validator