MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssralv Structured version   Visualization version   GIF version

Theorem ssralv 3650
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
Assertion
Ref Expression
ssralv (𝐴𝐵 → (∀𝑥𝐵 𝜑 → ∀𝑥𝐴 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv
StepHypRef Expression
1 ssel 3581 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . 2 (𝐴𝐵 → ((𝑥𝐵𝜑) → (𝑥𝐴𝜑)))
32ralimdv2 2956 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑 → ∀𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wral 2907  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-in 3566  df-ss 3573
This theorem is referenced by:  intss  4468  iinss1  4504  disjiun  4608  poss  5002  sess2  5048  isores3  6545  isoini2  6549  smores  7401  smores2  7403  tfrlem5  7428  resixp  7895  ac6sfi  8156  iunfi  8206  ixpfi2  8216  dffi3  8289  marypha1lem  8291  ordtypelem2  8376  tcrank  8699  acndom  8826  pwsdompw  8978  ssfin3ds  9104  fin1a2s  9188  hsmexlem4  9203  domtriomlem  9216  zornn0g  9279  fpwwe2lem13  9416  ingru  9589  cshw1  13513  rexanuz  14027  cau3lem  14036  caubnd  14040  limsupgord  14145  limsupval2  14153  rlimres  14231  lo1res  14232  o1of2  14285  o1rlimmul  14291  isercolllem1  14337  climsup  14342  fsumiun  14491  lcmfunsnlem1  15285  coprmprod  15310  pcfac  15538  vdwnnlem2  15635  firest  16025  imasaddfnlem  16120  imasvscafn  16129  psss  17146  tsrss  17155  cntz2ss  17697  cntzmhm2  17704  subgpgp  17944  efgsres  18083  telgsumfzs  18318  telgsums  18322  dprdss  18360  ocv2ss  19949  mretopd  20819  tgcn  20979  tgcnp  20980  subbascn  20981  cnss2  21004  cncnp  21007  sslm  21026  t1ficld  21054  tgcmp  21127  1stcfb  21171  islly2  21210  dislly  21223  comppfsc  21258  ptbasfi  21307  ptcnplem  21347  tx1stc  21376  qtoptop2  21425  fbunfip  21596  flftg  21723  txflf  21733  fclsbas  21748  fclsss1  21749  fclsss2  21750  alexsubb  21773  tmdgsum2  21823  metrest  22252  rescncf  22623  cnllycmp  22678  bndth  22680  fgcfil  22992  cfilres  23017  ivthlem2  23144  ivthlem3  23145  ovolsslem  23175  ovolfiniun  23192  finiunmbl  23235  volfiniun  23238  iunmbl  23244  ioombl1lem4  23252  dyadmax  23289  vitali  23305  mbfimaopnlem  23345  mbflimsup  23356  mbfi1flim  23413  ditgeq3  23537  dvferm  23672  rollelem  23673  dvivthlem1  23692  itgsubstlem  23732  aalioulem2  24009  ulmcaulem  24069  ulmss  24072  xrlimcnp  24612  lgsdchr  24997  pntlem3  25215  pntlemp  25216  pntleml  25217  uspgr2wlkeq  26428  redwlk  26455  wwlksm1edg  26653  wwlksnred  26673  clwlkclwwlklem2  26785  clwwlksf  26798  wwlksubclwwlks  26808  extwwlkfablem2  27085  occon  28016  xrge0infss  29392  resspos  29468  resstos  29469  submarchi  29549  sigaclci  30000  measiun  30086  elmbfmvol2  30134  sibfof  30207  ftc2re  30474  bnj1118  30795  subfacp1lem3  30907  iccllysconn  30975  untint  31332  untangtr  31334  dfon2lem6  31429  dfon2lem8  31431  dfon2lem9  31432  poseq  31486  soseq  31487  nosepon  31558  noreslege  31606  neibastop1  32031  neibastop2lem  32032  neibastop3  32034  finixpnum  33061  ptrecube  33076  poimirlem26  33102  poimirlem27  33103  poimirlem30  33106  heicant  33111  volsupnfl  33121  prdstotbnd  33260  heibor1lem  33275  ispridl2  33504  elrfirn2  36774  rabdiophlem1  36880  dford3lem1  37108  kelac1  37148  acsfn1p  37285  ssralv2  38254  ssralv2VD  38620  climinf  39270  limsupvaluz2  39402  supcnvlimsup  39404  iccpartres  40678
  Copyright terms: Public domain W3C validator