Theorem rspccva 3168

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

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
2	1	rspcv 3165	. 2 |- ( A e. B -> ( A. x e. B ph -> ps ) )
3	2	impcom 430	1 |- ( ( A. x e. B ph /\ A e. B ) -> ps )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   A.wral 2795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-v 3070

This theorem is referenced by:  disjne  3822  seex  4781  foelrn  5961  fconstfv  6039  grprinvlem  6401  caofid0l  6448  caofid0r  6449  caofid1  6450  caofid2  6451  onnseq  6905  odi  7118  omsmolem  7192  fvixp  7368  unblem1  7665  ordiso2  7830  unwdomg  7900  ac5num  8307  acni2  8317  fodomacn  8327  iundom2g  8805  fpwwe2lem3  8901  eltsk2g  9019  tskpwss  9020  tskpw  9021  tsken  9022  prlem934  9303  dedekindle  9635  ltord1  9967  leord1  9968  eqord1  9969  ltord2  9970  leord2  9971  eqord2  9972  supmul1  10396  seqcaopr2  11943  bccl  12199  hashbc  12308  limsupbnd2  13063  2clim  13152  climsup  13249  caurcvg2  13257  caucvgb  13259  isummulc2  13331  fsumtscopo2  13368  fsumparts  13371  incexclem  13401  isumshft  13404  climcndslem1  13414  climcndslem2  13415  supcvg  13420  geomulcvg  13438  mertenslem2  13447  mertens  13448  rpnnen2lem10  13608  dvdsprime  13878  iscatd2  14721  fuciso  14987  luble  15259  glble  15272  lubub  15391  lubl  15392  mgmlrid  15539  grpinvex  15655  issubg2  15798  issubg4  15802  nmzbi  15823  gagrpid  15914  cntzi  15949  psgnunilem2  16103  sylow1lem3  16203  pgpfi  16208  slwispgp  16214  sylow2alem1  16220  dprdfcl  16602  dprdfclOLD  16608  ablfac2  16695  abveq0  17017  issrngd  17052  psrbagconf1o  17550  pf1ind  17898  phllmhm  18170  ipcl  18171  ipeq0  18176  isphld  18192  ocvi  18203  elcls3  18803  neindisj2  18843  perfi  18875  cnima  18985  1stcfb  19165  1stcelcls  19181  llyi  19194  nllyi  19195  1stckgenlem  19242  ptbasin  19266  txcls  19293  ptcnp  19311  ufli  19603  tgpt0  19805  tsmsxplem2  19844  nrmmetd  20283  tngngp  20356  reperflem  20511  lebnumlem3  20651  htpyi  20662  htpycc  20668  phtpyi  20672  cfili  20895  cmetcvg  20912  caubl  20934  caublcls  20935  bcthlem2  20952  bcthlem3  20953  bcthlem4  20954  ovolicc2lem1  21116  ovolicc2lem5  21120  ovolicc2  21121  voliunlem3  21149  volsuplem  21152  uniioombllem2  21179  mbfima  21226  ismbfd  21234  ismbf3d  21248  mbfmullem  21319  itg2monolem1  21344  itg2i1fseqle  21348  itg2i1fseq  21349  itg2i1fseq2  21350  itg2addlem  21352  bddmulibl  21432  c1liplem1  21584  dvfsumle  21609  dvfsumabs  21611  dvfsumrlimf  21613  dvfsumlem1  21614  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumlem4  21617  dvfsumrlimge0  21618  dvfsum2  21622  ftc1lem6  21629  ulmcau  21976  ulmdvlem1  21981  ulmdvlem3  21983  mtestbdd  21986  itgulm  21989  radcnvlem1  21994  abelthlem5  22016  abelthlem7  22019  areambl  22468  dchrisumlem2  22855  dchrvmasumiflem1  22866  pntpbnd1  22951  ostthlem1  22992  tglowdim1i  23072  brbtwn2  23286  ax5seglem1  23309  ax5seglem2  23310  ax5seglem9  23318  axcontlem4  23348  axcontlem12  23356  usgrcyclnl1  23661  eupaseg  23729  grpoidinvlem3  23828  grpoidinv  23830  grpoidinv2  23840  isgrp2d  23857  cmpidelt  23951  rngoid  24005  vcid  24064  minvecolem5  24417  hcaucvg  24723  hlimconvi  24728  lnopeq0i  25546  cnlnadjlem5  25610  csmdsymi  25873  difelsiga  26710  eulerpartlemb  26885  ballotlemfc0  27009  ballotlemfcc  27010  ptpcon  27256  cvmsdisj  27293  cvmshmeo  27294  snmlflim  27355  sinccvg  27452  preddowncl  27791  bpolycl  28329  bpolydif  28332  mblfinlem1  28566  ovoliunnfl  28571  ex-ovoliunnfl  28572  voliunnfl  28573  volsupnfl  28574  mbfresfi  28576  itg2gt0cn  28585  bddiblnc  28600  ftc1cnnc  28604  ftc1anc  28613  locfinnei  28712  fnemeet1  28725  fnemeet2  28726  fnejoin1  28727  fnejoin2  28728  upixp  28761  filbcmb  28772  sdclem1  28777  seqpo  28781  incsequz2  28783  mettrifi  28791  caushft  28795  sstotbnd2  28811  heibor1lem  28846  heiborlem3  28850  heiborlem10  28857  heibor  28858  rrndstprj2  28868  limsuc2  29531  cncmpmax  29892  climinf  29917  climsuse  29919  stoweidlem7  29940  stoweidlem15  29948  stoweidlem21  29954  stoweidlem31  29964  stoweidlem35  29968  stoweidlem36  29969  stoweidlem50  29983  stoweidlem57  29990  stoweidlem59  29992  wallispilem3  30000  usgreghash2spot  30800  cayhamlem3  31342  bj-seex  32726