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

Theorem rspccva 3053
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 3050 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32impcom 421 1  |-  ( ( A. x  e.  B  ph 
/\  A  e.  B
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707
This theorem is referenced by:  disjne  3675  seex  4547  foelrn  5890  fconstfv  5956  grprinvlem  6287  caofid0l  6334  caofid0r  6335  caofid1  6336  caofid2  6337  onnseq  6608  odi  6824  omsmolem  6898  fvixp  7069  unblem1  7361  ordiso2  7486  unwdomg  7554  ac5num  7919  acni2  7929  fodomacn  7939  iundom2g  8417  fpwwe2lem3  8510  eltsk2g  8628  tskpwss  8629  tskpw  8630  tsken  8631  prlem934  8912  ltord1  9555  leord1  9556  eqord1  9557  ltord2  9558  leord2  9559  eqord2  9560  supmul1  9975  seqcaopr2  11361  bccl  11615  hashbc  11704  limsupbnd2  12279  2clim  12368  climsup  12465  caurcvg2  12473  caucvgb  12475  isummulc2  12548  fsumtscopo2  12584  fsumparts  12587  incexclem  12618  isumshft  12621  climcndslem1  12631  climcndslem2  12632  supcvg  12637  geomulcvg  12655  mertenslem2  12664  mertens  12665  rpnnen2lem10  12825  dvdsprime  13094  iscatd2  13908  fuciso  14174  lubub  14548  lubl  14549  mgmlrid  14714  grpinvex  14822  issubg2  14961  issubg4  14963  nmzbi  14982  gagrpid  15073  cntzi  15130  sylow1lem3  15236  pgpfi  15241  slwispgp  15247  sylow2alem1  15253  dprdfcl  15573  ablfac2  15649  abveq0  15916  issrngd  15951  psrbagconf1o  16441  phllmhm  16865  ipcl  16866  ipeq0  16871  isphld  16887  ocvi  16898  elcls3  17149  neindisj2  17189  perfi  17221  cnima  17331  1stcfb  17510  1stcelcls  17526  llyi  17539  nllyi  17540  1stckgenlem  17587  ptbasin  17611  txcls  17638  ptcnp  17656  ufli  17948  tgpt0  18150  tsmsxplem2  18185  nrmmetd  18624  tngngp  18697  reperflem  18851  lebnumlem3  18990  htpyi  19001  htpycc  19007  phtpyi  19011  cfili  19223  cmetcvg  19240  caubl  19262  caublcls  19263  bcthlem2  19280  bcthlem3  19281  bcthlem4  19282  ovolicc2lem1  19415  ovolicc2lem5  19419  ovolicc2  19420  voliunlem3  19448  volsuplem  19451  uniioombllem2  19477  mbfima  19526  ismbfd  19534  ismbf3d  19548  mbfmullem  19619  itg2monolem1  19644  itg2i1fseqle  19648  itg2i1fseq  19649  itg2i1fseq2  19650  itg2addlem  19652  bddmulibl  19732  c1liplem1  19882  dvfsumle  19907  dvfsumabs  19909  dvfsumrlimf  19911  dvfsumlem1  19912  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumlem4  19915  dvfsumrlimge0  19916  dvfsum2  19920  ftc1lem6  19927  pf1ind  19977  ulmcau  20313  ulmdvlem1  20318  ulmdvlem3  20320  mtestbdd  20323  itgulm  20326  radcnvlem1  20331  abelthlem5  20353  abelthlem7  20356  areambl  20799  dchrisumlem2  21186  dchrvmasumiflem1  21197  pntpbnd1  21282  ostthlem1  21323  usgrcyclnl1  21629  eupaseg  21697  grpoidinvlem3  21796  grpoidinv  21798  grpoidinv2  21808  isgrp2d  21825  cmpidelt  21919  rngoid  21973  vcid  22032  minvecolem5  22385  hcaucvg  22690  hlimconvi  22695  lnopeq0i  23512  cnlnadjlem5  23576  csmdsymi  23839  difelsiga  24518  ballotlemfc0  24752  ballotlemfcc  24753  ptpcon  24922  cvmsdisj  24959  cvmshmeo  24960  snmlflim  25021  sinccvg  25112  dedekindle  25190  preddowncl  25473  brbtwn2  25846  ax5seglem1  25869  ax5seglem2  25870  ax5seglem9  25878  axcontlem4  25908  axcontlem12  25916  bpolycl  26100  bpolydif  26103  mblfinlem1  26245  ovoliunnfl  26250  ex-ovoliunnfl  26251  voliunnfl  26252  volsupnfl  26253  mbfresfi  26255  itg2gt0cn  26262  bddiblnc  26277  ftc1cnnc  26281  ftc1anc  26290  locfinnei  26384  fnemeet1  26397  fnemeet2  26398  fnejoin1  26399  fnejoin2  26400  upixp  26433  filbcmb  26444  sdclem1  26449  seqpo  26453  incsequz2  26455  mettrifi  26465  caushft  26469  sstotbnd2  26485  heibor1lem  26520  heiborlem3  26524  heiborlem10  26531  heibor  26532  rrndstprj2  26542  limsuc2  27117  psgnunilem2  27397  cncmpmax  27681  climinf  27710  climsuse  27712  stoweidlem7  27734  stoweidlem15  27742  stoweidlem21  27748  stoweidlem31  27758  stoweidlem35  27762  stoweidlem36  27763  stoweidlem50  27777  stoweidlem57  27784  stoweidlem59  27786  wallispilem3  27794  usgreghash2spot  28520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960
  Copyright terms: Public domain W3C validator