Theorem rsp 2823

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Assertion

Ref	Expression
rsp

Proof of Theorem rsp

Step	Hyp	Ref	Expression
1		df-ral 2812	. 2
2		sp 1859	. 2
3	1, 2	sylbi 195	1

Syntax hints:  ->wi 4  A.wal 1393  e.wcel 1818  A.wral 2807

This theorem is referenced by:  rspa  2824  rspec  2825  r19.21bi  2826  rsp2  2831  r19.12  2983  reupick2  3783  rspn0  3797  dfiun2g  4362  iinss2  4382  invdisj  4441  trss  4554  reusv1  4652  reusv2lem1  4653  reusv2lem3  4655  reusv3  4660  ralxfrALT  4671  fvmptss  5964  ffnfv  6057  riota5f  6282  mpt2eq123  6356  peano5  6723  fun11iun  6760  tfr3  7087  tz7.48-1  7127  tz7.49  7129  nneneq  7720  scottex  8324  dfac2  8532  infpssrlem4  8707  fin23lem30  8743  fin23lem31  8744  hsmexlem2  8828  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  konigthlem  8964  winalim2  9095  nqereu  9328  dedekind  9765  dedekindle  9766  prodeq2ii  13720  vdwlem9  14507  mreiincl  14993  srgi  17163  ringi  17211  lbsextlem3  17806  lbsextlem4  17807  tgcl  19471  txindis  20135  alexsubALTlem3  20549  prdsxmslem2  21032  fsumcn  21374  lebnumlem1  21461  iscmet3lem1  21730  iscmet3lem2  21731  ovoliunlem2  21914  mbfimaopnlem  22062  limciun  22298  ftalem3  23348  ostth3  23823  mptelee  24198  ubthlem2  25787  esumcvg  28092  dfon2lem3  29217  dfon2lem7  29221  trpredmintr  29314  wfrlem4  29346  wfrlem12  29354  frr3g  29386  frrlem4  29390  frrlem11  29399  neibastop1  30177  cover2  30204  upixp  30220  indexdom  30225  filbcmb  30231  mettrifi  30250  mpt2bi123f  30571  mptfcl  30652  aomclem2  31001  hbtlem5  31077  refsumcn  31405  rfcnnnub  31411  mullimc  31622  mullimcf  31629  addlimc  31654  itgsubsticclem  31774  stoweidlem25  31807  stoweidlem52  31834  stoweidlem59  31841  stoweidlem62  31844  wallispilem3  31849  stirlinglem13  31868  fourierdlem73  31962  2reu1  32191  ffnafv  32256  trintALTVD  33680  trintALT  33681  bnj228  33790  bnj590  33968  bnj594  33970  bnj600  33977  bnj1128  34046  bnj1125  34048  bnj1145  34049  bnj1398  34090  bnj1417  34097  riotasvd  34687  glbconxN  35102  cdlemefr29exN  36128  cdlemk36  36639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-ral 2812