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

Theorem rspcva 3134
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 3132 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 436 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-v 3033
This theorem is referenced by:  rexraleqim  3153  fvn0ssdmfun  6028  fveqdmss  6032  fvcofneq  6045  caofinvl  6577  tfisi  6704  suppssov1  6966  wfr3g  7052  wfrlem17  7070  tfrlem1  7112  boxriin  7582  boxcutc  7583  marypha1lem  7965  marypha1  7966  supmo  7984  infmo  8029  wemaplem2  8080  unwdomg  8117  isinffi  8444  dfac9  8584  sornom  8725  fin23lem11  8765  fin1a2lem13  8860  axdc3lem2  8899  winalim2  9139  grothac  9273  nqereu  9372  infmrclOLD  10615  nnsub  10670  zextle  11032  xrsupsslem  11617  xrinfmsslem  11618  supxrunb1  11630  supxrunb2  11631  injresinjlem  12056  ssnn0fi  12235  suppssfz  12244  faclbnd4lem4  12519  ishashinf  12667  rexuz3  13488  cau3lem  13494  caubnd2  13497  o1co  13727  climcn1  13732  incexclem  13971  dvdsext  14433  cshwsidrepsw  15142  prdsbasprj  15448  mreintcl  15579  isacs2  15637  acsfiel  15638  initoeu1  15984  initoeu2  15989  termoeu1  15991  isdrs2  16262  lublecllem  16312  joinle  16338  meetle  16352  acsdrsel  16491  isacs4lem  16492  isacs5lem  16493  acsdrscl  16494  acsficl  16495  mgmidmo  16580  gsumval2  16601  mrcmndind  16691  symgfix2  17135  odeq  17277  gexid  17310  mplind  18802  gsummoncoe1  18975  psgndiflemB  19245  mdetunilem1  19714  m2detleiblem3  19731  m2detleiblem4  19732  cpmatmcllem  19819  mp2pm2mplem4  19910  cayleyhamilton1  19993  cmpsublem  20491  cmpsub  20492  hauscmplem  20498  cmpfii  20501  ptpjcn  20703  isufil2  21001  ufileu  21012  isucn2  21372  cfiluweak  21388  cuspcvg  21394  lpbl  21596  lmmbr  22306  caussi  22345  mdeglt  23093  deg1lt  23125  ply1divex  23166  plyco0  23225  dgrco  23308  emcllem7  24006  isppw2  24121  pntleme  24525  pntlemp  24527  tglowdim2ln  24775  nbcusgra  25270  uvtxnbgra  25300  wlkdvspthlem  25416  clwwlkf  25601  rusgranumwlks  25763  frgraunss  25802  vdn0frgrav2  25830  vdgn0frgrav2  25831  vdn1frgrav2  25832  vdgn1frgrav2  25833  frgrancvvdeqlem4  25840  frgraregorufr  25860  extwwlkfablem1  25881  grpoidinvlem3  26015  grpoideu  26018  lnconi  27767  rngurd  28625  tpr2rico  28792  esumiun  28989  ofcfeqd2  28996  0elsiga  29010  sigaclci  29028  dya2icoseg2  29173  signstfvneq0  29533  derangsn  29965  frr3g  30584  fwddifnp1  31003  poimirlem25  32029  poimirlem26  32030  poimirlem30  32034  poimirlem31  32035  poimirlem32  32036  heicant  32039  mblfinlem2  32042  ftc1anc  32089  fdc  32138  bndss  32182  isdrngo2  32261  divrngidl  32325  maxidlmax  32340  cdleme0nex  33927  dihglblem2N  34933  hgmapvs  35533  ismrcd1  35611  nacsfg  35618  isnacs3  35623  nacsfix  35625  mzpcl1  35642  mzpcl2  35643  mzpcong  35893  dnnumch1  35973  fnwe2lem2  35980  aomclem1  35983  aomclem4  35986  aomclem6  35988  lnr2i  36046  hbtlem5  36058  hbt  36060  pwssfi  37441  eliind  37474  choicefi  37552  fsneq  37558  suplesup  37649  xralrple2  37664  infxr  37677  infleinf  37682  islpcn  37816  limclner  37829  cncfshift  37848  cncfperiod  37853  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem1OLD  37902  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  fourierdlem103  38185  fourierdlem104  38186  etransclem48OLD  38259  etransclem48  38260  salunicl  38289  saluncl  38290  saldifcl  38292  sge0pnffigt  38352  meadjuni  38411  omessle  38438  caragensplit  38440  omeunile  38445  hoidmvlelem2  38536  hoidmvlelem3  38537  hoidmvle  38540  vonvolmbllem  38600  vonvolmbl  38601  iccpartimp  38876  iccpartrn  38889  iccpartiun  38893  icceuelpart  38895  reuccatpfxs1  39122  n0snor2el  39143  uvtxanbgrvtx  39629  eupthseg  40119  upgreupthseg  40122  lidldomn1  40429  ply1mulgsumlem2  40687  lindslinindsimp2lem5  40763  lindslinindsimp2  40764  snlindsntor  40772  nn0sumshdiglemA  40938  nn0sumshdiglemB  40939  nn0sumshdig  40942
  Copyright terms: Public domain W3C validator