Theorem ssralv 3563

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv

Distinct variable groups:   ,   ,

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3497	. . 3
2	1	imim1d 75	. 2
3	2	ralimdv2 2864	1

Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807  C_wss 3475

This theorem is referenced by:  intss  4307  iinss1  4343  disjiun  4442  poss  4807  sess2  4853  isores3  6231  isoini2  6235  smores  7042  smores2  7044  tfrlem5  7068  resixp  7524  ac6sfi  7784  iunfi  7828  ixpfi2  7838  dffi3  7911  marypha1lem  7913  ordtypelem2  7965  tcrank  8323  acndom  8453  pwsdompw  8605  ssfin3ds  8731  fin1a2s  8815  hsmexlem4  8830  domtriomlem  8843  zornn0g  8906  fpwwe2lem13  9041  ingru  9214  cshw1  12790  rexanuz  13178  cau3lem  13187  caubnd  13191  limsupgord  13295  limsupval2  13303  rlimres  13381  lo1res  13382  o1of2  13435  o1rlimmul  13441  isercolllem1  13487  climsup  13492  fsumiun  13635  pcfac  14418  vdwnnlem2  14514  firest  14830  imasaddfnlem  14925  imasvscafn  14934  psss  15844  tsrss  15853  cntz2ss  16370  cntzmhm2  16377  subgpgp  16617  efgsres  16756  telgsumfzs  17018  telgsums  17022  dprdss  17076  ocv2ss  18704  mretopd  19593  tgcn  19753  tgcnp  19754  subbascn  19755  cnss2  19778  cncnp  19781  sslm  19800  t1ficld  19828  tgcmp  19901  1stcfb  19946  islly2  19985  dislly  19998  comppfsc  20033  ptbasfi  20082  ptcnplem  20122  tx1stc  20151  qtoptop2  20200  fbunfip  20370  flftg  20497  txflf  20507  fclsbas  20522  fclsss1  20523  fclsss2  20524  alexsubb  20546  tmdgsum2  20595  metrest  21027  rescncf  21401  cnllycmp  21456  bndth  21458  fgcfil  21710  cfilres  21735  ivthlem2  21864  ivthlem3  21865  ovolsslem  21895  ovolfiniun  21912  finiunmbl  21954  volfiniun  21957  iunmbl  21963  ioombl1lem4  21971  dyadmax  22007  vitali  22022  mbfimaopnlem  22062  mbflimsup  22073  mbfi1flim  22130  ditgeq3  22254  dvferm  22389  rollelem  22390  dvivthlem1  22409  itgsubstlem  22449  aalioulem2  22729  ulmcaulem  22789  ulmss  22792  xrlimcnp  23298  lgsdchr  23623  pntlem3  23794  pntlemp  23795  pntleml  23796  nbgraf1olem1  24441  redwlk  24608  usg2wlkeq  24708  wwlknred  24723  wwlkm1edg  24735  clwlkisclwwlklem1  24787  clwwlkf  24794  wwlksubclwwlk  24804  extwwlkfablem2  25078  occon  26205  xrge0infss  27580  resspos  27647  resstos  27648  submarchi  27730  sigaclci  28132  measiun  28189  elmbfmvol2  28238  sibfof  28282  subfacp1lem3  28626  iccllyscon  28695  untint  29084  untangtr  29086  dfon2lem6  29220  dfon2lem8  29222  dfon2lem9  29223  setlikess  29275  poseq  29333  soseq  29334  finixpnum  30038  heicant  30049  volsupnfl  30059  neibastop1  30177  neibastop2lem  30178  neibastop3  30180  prdstotbnd  30290  heibor1lem  30305  ispridl2  30435  elrfirn2  30628  rabdiophlem1  30734  dford3lem1  30968  kelac1  31009  acsfn1p  31148  climinf  31612  ssralv2  33301  ssralv2VD  33666  bnj1118  34040

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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-in 3482  df-ss 3489