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

Theorem ssralv 4011
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 3938 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . 2 (𝐴𝐵 → ((𝑥𝐵𝜑) → (𝑥𝐴𝜑)))
32ralimdv2 3157 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑 → ∀𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3061  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-v 3446  df-in 3918  df-ss 3928
This theorem is referenced by:  ss2ralv  4013  intss  4931  iinss1  4970  disjiun  5093  poss  5548  sess2  5603  isores3  7281  isoini2  7285  xpord2indlem  8080  xpord3inddlem  8087  poseq  8091  soseq  8092  smores  8299  smores2  8301  tfrlem5  8327  naddssim  8632  resixp  8874  ac6sfi  9234  iunfi  9287  ixpfi2  9297  marypha1lem  9374  ordtypelem2  9460  ttrclselem2  9667  tcrank  9825  acndom  9992  pwsdompw  10145  ssfin3ds  10271  fin1a2s  10355  hsmexlem4  10370  domtriomlem  10383  zornn0g  10446  fpwwe2lem12  10583  ingru  10756  cshw1  14716  rexanuz  15236  cau3lem  15245  caubnd  15249  limsupgord  15360  limsupval2  15368  rlimres  15446  lo1res  15447  o1of2  15501  o1rlimmul  15507  climsup  15560  fsumiun  15711  lcmfunsnlem1  16518  coprmprod  16542  pcfac  16776  vdwnnlem2  16873  firest  17319  imasaddfnlem  17415  imasvscafn  17424  psss  18474  tsrss  18483  cntz2ss  19118  cntzmhm2  19125  subgpgp  19384  efgsres  19525  telgsumfzs  19771  telgsums  19775  dprdss  19813  acsfn1p  20280  ocv2ss  21093  mretopd  22459  tgcn  22619  tgcnp  22620  subbascn  22621  cnss2  22644  cncnp  22647  sslm  22666  t1ficld  22694  tgcmp  22768  1stcfb  22812  islly2  22851  dislly  22864  comppfsc  22899  ptbasfi  22948  ptcnplem  22988  tx1stc  23017  qtoptop2  23066  fbunfip  23236  flftg  23363  txflf  23373  fclsbas  23388  fclsss1  23389  fclsss2  23390  alexsubb  23413  tmdgsum2  23463  metrest  23896  rescncf  24276  cnllycmp  24335  bndth  24337  fgcfil  24651  ivthlem2  24832  ivthlem3  24833  ovolsslem  24864  ovolfiniun  24881  finiunmbl  24924  volfiniun  24927  iunmbl  24933  ioombl1lem4  24941  dyadmax  24978  vitali  24993  mbfimaopnlem  25035  mbflimsup  25046  mbfi1flim  25104  ditgeq3  25230  dvferm  25368  rollelem  25369  dvivthlem1  25388  itgsubstlem  25428  aalioulem2  25709  ulmcaulem  25769  ulmss  25772  xrlimcnp  26334  2sqreunnlem2  26819  pntlem3  26973  pntlemp  26974  pntleml  26975  nosepon  27029  noresle  27061  sssslt1  27156  sssslt2  27157  uspgr2wlkeq  28636  redwlk  28662  wwlksm1edg  28868  wwlksnred  28879  clwlkclwwlklem2  28986  clwwlkinwwlk  29026  clwwlkf  29033  wwlksubclwwlk  29044  occon  30271  xrge0infss  31712  resspos  31875  resstos  31876  gsummptres2  31944  submarchi  32071  prmidl2  32261  sigaclci  32788  measiun  32874  elmbfmvol2  32924  sibfof  32997  ftc2re  33268  bnj1118  33653  subfacp1lem3  33833  iccllysconn  33901  dmopab3rexdif  34056  untint  34340  untangtr  34342  dfon2lem6  34419  dfon2lem8  34421  dfon2lem9  34422  neibastop1  34877  neibastop2lem  34878  neibastop3  34880  finixpnum  36109  ptrecube  36124  poimirlem26  36150  poimirlem27  36151  poimirlem30  36154  heicant  36159  volsupnfl  36169  prdstotbnd  36299  heibor1lem  36314  ispridl2  36543  elrfirn2  41062  rabdiophlem1  41167  dford3lem1  41393  kelac1  41433  ssralv2  42901  ssralv2VD  43236  climinf  43933  limsupvaluz2  44065  supcnvlimsup  44067  iccpartres  45696
  Copyright terms: Public domain W3C validator