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

Theorem rspcva 3051
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 3049 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 420 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2706
This theorem is referenced by:  tfisi  4839  suppssov1  6303  caofinvl  6332  boxriin  7105  boxcutc  7106  marypha1lem  7439  marypha1  7440  supmo  7458  wemaplem2  7517  unwdomg  7553  noinfepOLD  7616  isinffi  7880  dfac9  8017  sornom  8158  fin23lem11  8198  fin1a2lem13  8293  axdc3lem2  8332  winalim2  8572  grothac  8706  nqereu  8807  infmrcl  9988  nnsub  10039  zextle  10344  xrsupsslem  10886  xrinfmsslem  10887  supxrunb1  10899  supxrunb2  10900  injresinjlem  11200  faclbnd4lem4  11588  rexuz3  12153  cau3lem  12159  caubnd2  12162  o1co  12381  climcn1  12386  incexclem  12617  dvdsext  12901  prdsbasprj  13695  mreintcl  13821  isacs2  13879  acsfiel  13880  isdrs2  14397  lubid  14440  acsdrsel  14594  isacs4lem  14595  isacs5lem  14596  acsdrscl  14597  acsficl  14598  mgmidmo  14694  gsumval2  14784  odeq  15189  gexid  15216  mplind  16563  cmpsublem  17463  cmpsub  17464  hauscmplem  17470  cmpfii  17473  ptpjcn  17644  isufil2  17941  ufileu  17952  cfiluweak  18326  cuspcvg  18332  lpbl  18534  lmmbr  19212  caussi  19251  evlslem1  19937  mdeglt  19989  deg1lt  20021  ply1divex  20060  plyco0  20112  dgrco  20194  emcllem7  20841  isppw2  20899  pntleme  21303  pntlemp  21305  nbcusgra  21473  uvtxnbgra  21503  wlkdvspthlem  21608  grpoidinvlem3  21795  grpoideu  21798  lnconi  23537  ishashinf  24160  kerf1hrm  24263  tpr2rico  24311  ofcfeqd2  24485  0elsiga  24498  sigaclci  24516  dya2icoseg2  24629  derangsn  24857  wfr3g  25538  frr3g  25582  mblfinlem2  26245  ftc1anc  26289  fdc  26450  bndss  26496  isdrngo2  26575  divrngidl  26639  maxidlmax  26654  ismrcd1  26753  nacsfg  26760  isnacs3  26765  nacsfix  26767  mzpcl1  26787  mzpcl2  26788  mzpcong  27038  dnnumch1  27120  fnwe2lem2  27127  aomclem1  27130  aomclem4  27133  aomclem6  27135  lnr2i  27298  hbtlem5  27310  hbt  27312  frgraunss  28386  vdn0frgrav2  28415  vdgn0frgrav2  28416  vdn1frgrav2  28417  vdgn1frgrav2  28418  frgrancvvdeqlem4  28423  frgraregorufr  28443  cdleme0nex  31088  dihglblem2N  32093  hgmapvs  32693
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 2418
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 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-v 2959
  Copyright terms: Public domain W3C validator