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

Theorem rspcva 3148
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 3146 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 431 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444    e. wcel 1887   A.wral 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047
This theorem is referenced by:  rexraleqim  3165  fvn0ssdmfun  6013  fveqdmss  6017  fvcofneq  6030  caofinvl  6558  tfisi  6685  suppssov1  6947  wfr3g  7034  wfrlem17  7052  tfrlem1  7094  boxriin  7564  boxcutc  7565  marypha1lem  7947  marypha1  7948  supmo  7966  infmo  8011  wemaplem2  8062  unwdomg  8099  isinffi  8426  dfac9  8566  sornom  8707  fin23lem11  8747  fin1a2lem13  8842  axdc3lem2  8881  winalim2  9121  grothac  9255  nqereu  9354  infmrclOLD  10593  nnsub  10648  zextle  11009  xrsupsslem  11592  xrinfmsslem  11593  supxrunb1  11605  supxrunb2  11606  injresinjlem  12024  ssnn0fi  12197  suppssfz  12206  faclbnd4lem4  12481  ishashinf  12626  rexuz3  13411  cau3lem  13417  caubnd2  13420  o1co  13650  climcn1  13655  incexclem  13894  dvdsext  14356  cshwsidrepsw  15064  prdsbasprj  15370  mreintcl  15501  isacs2  15559  acsfiel  15560  initoeu1  15906  initoeu2  15911  termoeu1  15913  isdrs2  16184  lublecllem  16234  joinle  16260  meetle  16274  acsdrsel  16413  isacs4lem  16414  isacs5lem  16415  acsdrscl  16416  acsficl  16417  mgmidmo  16502  gsumval2  16523  mrcmndind  16613  symgfix2  17057  odeq  17199  gexid  17232  mplind  18725  evlslem1  18738  gsummoncoe1  18898  psgndiflemB  19168  mdetunilem1  19637  m2detleiblem3  19654  m2detleiblem4  19655  cpmatmcllem  19742  mp2pm2mplem4  19833  cayleyhamilton1  19916  cmpsublem  20414  cmpsub  20415  hauscmplem  20421  cmpfii  20424  ptpjcn  20626  isufil2  20923  ufileu  20934  isucn2  21294  cfiluweak  21310  cuspcvg  21316  lpbl  21518  lmmbr  22228  caussi  22267  mdeglt  23014  deg1lt  23046  ply1divex  23087  plyco0  23146  dgrco  23229  emcllem7  23927  isppw2  24042  pntleme  24446  pntlemp  24448  tglowdim2ln  24696  nbcusgra  25191  uvtxnbgra  25221  wlkdvspthlem  25337  clwwlkf  25522  rusgranumwlks  25684  frgraunss  25723  vdn0frgrav2  25751  vdgn0frgrav2  25752  vdn1frgrav2  25753  vdgn1frgrav2  25754  frgrancvvdeqlem4  25761  frgraregorufr  25781  extwwlkfablem1  25802  grpoidinvlem3  25934  grpoideu  25937  lnconi  27686  rngurd  28551  tpr2rico  28718  esumiun  28915  ofcfeqd2  28922  0elsiga  28936  sigaclci  28954  dya2icoseg2  29100  signstfvneq0  29461  derangsn  29893  frr3g  30513  fwddifnp1  30932  poimirlem25  31965  poimirlem26  31966  poimirlem30  31970  poimirlem31  31971  poimirlem32  31972  heicant  31975  mblfinlem2  31978  ftc1anc  32025  fdc  32074  bndss  32118  isdrngo2  32197  divrngidl  32261  maxidlmax  32276  cdleme0nex  33856  dihglblem2N  34862  hgmapvs  35462  ismrcd1  35540  nacsfg  35547  isnacs3  35552  nacsfix  35554  mzpcl1  35571  mzpcl2  35572  mzpcong  35822  dnnumch1  35902  fnwe2lem2  35909  aomclem1  35912  aomclem4  35915  aomclem6  35917  lnr2i  35975  hbtlem5  35987  hbt  35989  pwssfi  37381  eliind  37415  choicefi  37481  suplesup  37562  xralrple2  37577  islpcn  37719  limclner  37732  cncfshift  37751  cncfperiod  37756  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem1OLD  37805  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  fourierdlem103  38073  fourierdlem104  38074  etransclem48OLD  38147  etransclem48  38148  salunicl  38177  saluncl  38178  saldifcl  38180  sge0pnffigt  38238  meadjuni  38295  omessle  38319  caragensplit  38321  omeunile  38326  hoidmvlelem2  38418  hoidmvlelem3  38419  hoidmvle  38422  iccpartimp  38731  iccpartrn  38744  iccpartiun  38748  icceuelpart  38750  reuccatpfxs1  38975  n0snor2el  38996  uvtxanbgrvtx  39465  lidldomn1  39974  ply1mulgsumlem2  40232  lindslinindsimp2lem5  40308  lindslinindsimp2  40309  snlindsntor  40317  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484  nn0sumshdig  40487
  Copyright terms: Public domain W3C validator