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

Theorem rspcva 3018
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 3016 . 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 1649    e. wcel 1721   A.wral 2674
This theorem is referenced by:  tfisi  4805  suppssov1  6269  caofinvl  6298  boxriin  7071  boxcutc  7072  marypha1lem  7404  marypha1  7405  supmo  7421  wemaplem2  7480  unwdomg  7516  noinfepOLD  7579  isinffi  7843  dfac9  7980  sornom  8121  fin23lem11  8161  fin1a2lem13  8256  axdc3lem2  8295  winalim2  8535  grothac  8669  nqereu  8770  infmrcl  9951  nnsub  10002  zextle  10307  xrsupsslem  10849  xrinfmsslem  10850  supxrunb1  10862  supxrunb2  10863  injresinjlem  11162  faclbnd4lem4  11550  rexuz3  12115  cau3lem  12121  caubnd2  12124  o1co  12343  climcn1  12348  incexclem  12579  dvdsext  12863  prdsbasprj  13657  mreintcl  13783  isacs2  13841  acsfiel  13842  isdrs2  14359  lubid  14402  acsdrsel  14556  isacs4lem  14557  isacs5lem  14558  acsdrscl  14559  acsficl  14560  mgmidmo  14656  gsumval2  14746  odeq  15151  gexid  15178  mplind  16525  cmpsublem  17424  cmpsub  17425  hauscmplem  17431  cmpfii  17434  ptpjcn  17604  isufil2  17901  ufileu  17912  cfiluweak  18286  cuspcvg  18292  lpbl  18494  lmmbr  19172  caussi  19211  evlslem1  19897  mdeglt  19949  deg1lt  19981  ply1divex  20020  plyco0  20072  dgrco  20154  emcllem7  20801  isppw2  20859  pntleme  21263  pntlemp  21265  nbcusgra  21433  uvtxnbgra  21463  wlkdvspthlem  21568  grpoidinvlem3  21755  grpoideu  21758  lnconi  23497  ishashinf  24120  kerf1hrm  24223  tpr2rico  24271  ofcfeqd2  24445  0elsiga  24458  sigaclci  24476  dya2icoseg2  24589  derangsn  24817  wfr3g  25477  frr3g  25502  mblfinlem  26151  fdc  26347  bndss  26393  isdrngo2  26472  divrngidl  26536  maxidlmax  26551  ismrcd1  26650  nacsfg  26657  isnacs3  26662  nacsfix  26664  mzpcl1  26684  mzpcl2  26685  mzpcong  26935  dnnumch1  27017  fnwe2lem2  27024  aomclem1  27027  aomclem4  27030  aomclem6  27032  lnr2i  27196  hbtlem5  27208  hbt  27210  frgraunss  28107  vdn0frgrav2  28136  vdgn0frgrav2  28137  vdn1frgrav2  28138  vdgn1frgrav2  28139  frgrancvvdeqlem4  28144  frgraregorufr  28164  cdleme0nex  30784  dihglblem2N  31789  hgmapvs  32389
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 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-v 2926
  Copyright terms: Public domain W3C validator